aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics
ModeNameSize
-rw-r--r--.cvsignore9logplain
-rw-r--r--auto.ml30463logplain
-rw-r--r--auto.mli6259logplain
-rw-r--r--autorewrite.ml3435logplain
-rw-r--r--autorewrite.mli851logplain
-rw-r--r--btermdn.ml1521logplain
-rw-r--r--btermdn.mli893logplain
-rw-r--r--contradiction.ml2659logplain
-rw-r--r--contradiction.mli719logplain
-rw-r--r--dhyp.ml11418logplain
-rw-r--r--dhyp.mli1119logplain
-rw-r--r--dn.ml2915logplain
-rw-r--r--dn.mli1739logplain
-rw-r--r--doc.tex246logplain
-rw-r--r--eauto.ml413865logplain
-rw-r--r--eauto.mli840logplain
-rw-r--r--elim.ml5612logplain
-rw-r--r--elim.mli1375logplain
-rw-r--r--eqdecide.ml45874logplain
-rw-r--r--equality.ml44173logplain
-rw-r--r--equality.mli2900logplain
-rw-r--r--extraargs.ml4922logplain
-rw-r--r--extraargs.mli726logplain
-rw-r--r--extratactics.ml46561logplain
-rw-r--r--extratactics.mli760logplain
-rw-r--r--hiddentac.ml4424logplain
-rw-r--r--hiddentac.mli3817logplain
-rw-r--r--hipattern.ml11595logplain
-rw-r--r--hipattern.mli4830logplain
-rw-r--r--inv.ml19392logplain
-rw-r--r--inv.mli1458logplain
-rw-r--r--leminv.ml10510logplain
-rw-r--r--leminv.mli528logplain
-rw-r--r--nbtermdn.ml2556logplain
-rw-r--r--nbtermdn.mli1328logplain
-rw-r--r--refine.ml10903logplain
-rw-r--r--refine.mli602logplain
-rw-r--r--setoid_replace.ml23880logplain
-rw-r--r--setoid_replace.mli942logplain
-rw-r--r--tacinterp.ml80974logplain
-rw-r--r--tacinterp.mli4120logplain
-rw-r--r--tacticals.ml15142logplain
-rw-r--r--tacticals.mli6376logplain
-rw-r--r--tactics.ml69021logplain
-rw-r--r--tactics.mli8869logplain
-rw-r--r--tauto.ml46154logplain
-rw-r--r--termdn.ml2345logplain
-rw-r--r--termdn.mli1621logplain