Library GeoCoq.Tactics.finish

Ltac finish := auto with between between_no_eauto col out par perp cong midpoint side conga lea suma sums circle gravitycenter cop.

Create HintDb between.
Create HintDb between_no_eauto.
Create HintDb col.
Create HintDb out.
Create HintDb par.
Create HintDb perp.
Create HintDb cong.
Create HintDb midpoint.
Create HintDb side.
Create HintDb conga.
Create HintDb lea.
Create HintDb suma.
Create HintDb sums.
Create HintDb circle.
Create HintDb gravitycenter.
Create HintDb cop.