summaryrefslogtreecommitdiff
path: root/tactics
ModeNameSize
-rw-r--r--auto.ml29373logplain
-rw-r--r--auto.mli6248logplain
-rw-r--r--autorewrite.ml6280logplain
-rw-r--r--autorewrite.mli1027logplain
-rw-r--r--btermdn.ml1594logplain
-rw-r--r--btermdn.mli949logplain
-rw-r--r--contradiction.ml2720logplain
-rw-r--r--contradiction.mli781logplain
-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.ml42194logplain
-rw-r--r--equality.mli4256logplain
-rw-r--r--evar_tactics.ml2489logplain
-rw-r--r--evar_tactics.mli841logplain
-rw-r--r--extraargs.ml43641logplain
-rw-r--r--extraargs.mli1522logplain
-rw-r--r--extratactics.ml414681logplain
-rw-r--r--extratactics.mli1267logplain
-rw-r--r--hiddentac.ml4539logplain
-rw-r--r--hiddentac.mli3656logplain
-rw-r--r--hipattern.ml411180logplain
-rw-r--r--hipattern.mli4808logplain
-rw-r--r--inv.ml19312logplain
-rw-r--r--inv.mli1497logplain
-rw-r--r--leminv.ml10675logplain
-rw-r--r--leminv.mli545logplain
-rw-r--r--nbtermdn.ml2634logplain
-rw-r--r--nbtermdn.mli1403logplain
-rw-r--r--refine.ml10948logplain
-rw-r--r--refine.mli639logplain
-rw-r--r--setoid_replace.ml76011logplain
-rw-r--r--setoid_replace.mli2794logplain
-rw-r--r--tacinterp.ml89860logplain
-rw-r--r--tacinterp.mli4519logplain
-rw-r--r--tacticals.ml15176logplain
-rw-r--r--tacticals.mli6442logplain
-rw-r--r--tactics.ml89448logplain
-rw-r--r--tactics.mli11689logplain
-rw-r--r--tauto.ml45429logplain
-rw-r--r--termdn.ml2311logplain
-rw-r--r--termdn.mli1698logplain