summaryrefslogtreecommitdiff
path: root/tactics
ModeNameSize
-rw-r--r--auto.ml29413logplain
-rw-r--r--auto.mli6248logplain
-rw-r--r--autorewrite.ml7687logplain
-rw-r--r--autorewrite.mli1178logplain
-rw-r--r--btermdn.ml1594logplain
-rw-r--r--btermdn.mli949logplain
-rw-r--r--contradiction.ml2938logplain
-rw-r--r--contradiction.mli781logplain
-rw-r--r--decl_interp.ml16834logplain
-rw-r--r--decl_interp.mli770logplain
-rw-r--r--decl_proof_instr.ml46835logplain
-rw-r--r--decl_proof_instr.mli3826logplain
-rw-r--r--dhyp.ml11435logplain
-rw-r--r--dhyp.mli1172logplain
-rw-r--r--dn.ml2965logplain
-rw-r--r--dn.mli1790logplain
-rw-r--r--doc.tex246logplain
-rw-r--r--eauto.ml413353logplain
-rw-r--r--eauto.mli1040logplain
-rw-r--r--elim.ml5648logplain
-rw-r--r--elim.mli1432logplain
-rw-r--r--eqdecide.ml46428logplain
-rw-r--r--equality.ml43039logplain
-rw-r--r--equality.mli4311logplain
-rw-r--r--evar_tactics.ml2477logplain
-rw-r--r--evar_tactics.mli841logplain
-rw-r--r--extraargs.ml46451logplain
-rw-r--r--extraargs.mli2212logplain
-rw-r--r--extratactics.ml413950logplain
-rw-r--r--extratactics.mli838logplain
-rw-r--r--hiddentac.ml4627logplain
-rw-r--r--hiddentac.mli3699logplain
-rw-r--r--hipattern.ml411180logplain
-rw-r--r--hipattern.mli4808logplain
-rw-r--r--inv.ml19312logplain
-rw-r--r--inv.mli1497logplain
-rw-r--r--leminv.ml10680logplain
-rw-r--r--leminv.mli545logplain
-rw-r--r--nbtermdn.ml2634logplain
-rw-r--r--nbtermdn.mli1403logplain
-rw-r--r--refine.ml11052logplain
-rw-r--r--refine.mli639logplain
-rw-r--r--setoid_replace.ml77326logplain
-rw-r--r--setoid_replace.mli2848logplain
-rw-r--r--tacinterp.ml99949logplain
-rw-r--r--tacinterp.mli4880logplain
-rw-r--r--tacticals.ml15224logplain
-rw-r--r--tacticals.mli6495logplain
-rw-r--r--tactics.ml92770logplain
-rw-r--r--tactics.mli11876logplain
-rw-r--r--tauto.ml45429logplain
-rw-r--r--termdn.ml2311logplain
-rw-r--r--termdn.mli1698logplain