summaryrefslogtreecommitdiff
path: root/tactics
ModeNameSize
-rw-r--r--auto.ml30287logplain
-rw-r--r--auto.mli6320logplain
-rw-r--r--autorewrite.ml3379logplain
-rw-r--r--autorewrite.mli920logplain
-rw-r--r--btermdn.ml1585logplain
-rw-r--r--btermdn.mli958logplain
-rw-r--r--contradiction.ml2728logplain
-rw-r--r--contradiction.mli789logplain
-rw-r--r--dhyp.ml11479logplain
-rw-r--r--dhyp.mli1180logplain
-rw-r--r--dn.ml2974logplain
-rw-r--r--dn.mli1799logplain
-rw-r--r--doc.tex246logplain
-rw-r--r--eauto.ml413928logplain
-rw-r--r--eauto.mli847logplain
-rw-r--r--elim.ml5685logplain
-rw-r--r--elim.mli1441logplain
-rw-r--r--eqdecide.ml45941logplain
-rw-r--r--equality.ml41527logplain
-rw-r--r--equality.mli2808logplain
-rw-r--r--extraargs.ml4988logplain
-rw-r--r--extraargs.mli794logplain
-rw-r--r--extratactics.ml49241logplain
-rw-r--r--extratactics.mli832logplain
-rw-r--r--hiddentac.ml4502logplain
-rw-r--r--hiddentac.mli3902logplain
-rw-r--r--hipattern.ml11669logplain
-rw-r--r--hipattern.mli4897logplain
-rw-r--r--inv.ml19468logplain
-rw-r--r--inv.mli1541logplain
-rw-r--r--leminv.ml10573logplain
-rw-r--r--leminv.mli528logplain
-rw-r--r--nbtermdn.ml2621logplain
-rw-r--r--nbtermdn.mli1394logplain
-rw-r--r--refine.ml10968logplain
-rw-r--r--refine.mli665logplain
-rw-r--r--setoid_replace.ml23950logplain
-rw-r--r--setoid_replace.mli1015logplain
-rw-r--r--tacinterp.ml86095logplain
-rw-r--r--tacinterp.mli4197logplain
-rw-r--r--tacticals.ml15241logplain
-rw-r--r--tacticals.mli6463logplain
-rw-r--r--tactics.ml70149logplain
-rw-r--r--tactics.mli9023logplain
-rw-r--r--tauto.ml46217logplain
-rw-r--r--termdn.ml2408logplain
-rw-r--r--termdn.mli1685logplain