summaryrefslogtreecommitdiff
path: root/tactics
ModeNameSize
-rw-r--r--auto.ml32847logplain
-rw-r--r--auto.mli6882logplain
-rw-r--r--autorewrite.ml7922logplain
-rw-r--r--autorewrite.mli1178logplain
-rw-r--r--btermdn.ml1594logplain
-rw-r--r--btermdn.mli949logplain
-rw-r--r--class_tactics.ml462642logplain
-rw-r--r--contradiction.ml2950logplain
-rw-r--r--contradiction.mli794logplain
-rw-r--r--decl_interp.ml16805logplain
-rw-r--r--decl_interp.mli824logplain
-rw-r--r--decl_proof_instr.ml46256logplain
-rw-r--r--decl_proof_instr.mli3785logplain
-rw-r--r--dhyp.ml11530logplain
-rw-r--r--dhyp.mli1172logplain
-rw-r--r--dn.ml2965logplain
-rw-r--r--dn.mli1790logplain
-rw-r--r--doc.tex246logplain
-rw-r--r--eauto.ml414417logplain
-rw-r--r--eauto.mli1095logplain
-rw-r--r--elim.ml5711logplain
-rw-r--r--elim.mli1432logplain
-rw-r--r--eqdecide.ml46391logplain
-rw-r--r--equality.ml48541logplain
-rw-r--r--equality.mli5026logplain
-rw-r--r--evar_tactics.ml2535logplain
-rw-r--r--evar_tactics.mli841logplain
-rw-r--r--extraargs.ml412348logplain
-rw-r--r--extraargs.mli2685logplain
-rw-r--r--extratactics.ml417968logplain
-rw-r--r--extratactics.mli743logplain
-rw-r--r--hiddentac.ml5878logplain
-rw-r--r--hiddentac.mli4276logplain
-rw-r--r--hipattern.ml411180logplain
-rw-r--r--hipattern.mli4808logplain
-rw-r--r--inv.ml19402logplain
-rw-r--r--inv.mli1497logplain
-rw-r--r--leminv.ml10673logplain
-rw-r--r--leminv.mli545logplain
-rw-r--r--nbtermdn.ml2635logplain
-rw-r--r--nbtermdn.mli1403logplain
-rw-r--r--refine.ml12359logplain
-rw-r--r--refine.mli639logplain
-rw-r--r--setoid_replace.ml78523logplain
-rw-r--r--setoid_replace.mli2955logplain
-rw-r--r--tacinterp.ml106886logplain
-rw-r--r--tacinterp.mli5336logplain
-rw-r--r--tacticals.ml14873logplain
-rw-r--r--tacticals.mli6672logplain
-rw-r--r--tactics.ml108181logplain
-rw-r--r--tactics.mli13416logplain
-rw-r--r--tauto.ml45430logplain
-rw-r--r--termdn.ml2311logplain
-rw-r--r--termdn.mli1698logplain