summaryrefslogtreecommitdiff
path: root/tactics
ModeNameSize
-rw-r--r--auto.ml30524logplain
-rw-r--r--auto.mli6321logplain
-rw-r--r--autorewrite.ml3442logplain
-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.ml41299logplain
-rw-r--r--equality.mli2808logplain
-rw-r--r--extraargs.ml4988logplain
-rw-r--r--extraargs.mli792logplain
-rw-r--r--extratactics.ml49266logplain
-rw-r--r--extratactics.mli830logplain
-rw-r--r--hiddentac.ml4502logplain
-rw-r--r--hiddentac.mli3900logplain
-rw-r--r--hipattern.ml11669logplain
-rw-r--r--hipattern.mli4897logplain
-rw-r--r--inv.ml19476logplain
-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.mli1013logplain
-rw-r--r--tacinterp.ml85049logplain
-rw-r--r--tacinterp.mli4197logplain
-rw-r--r--tacticals.ml15241logplain
-rw-r--r--tacticals.mli6463logplain
-rw-r--r--tactics.ml69742logplain
-rw-r--r--tactics.mli9017logplain
-rw-r--r--tauto.ml46217logplain
-rw-r--r--termdn.ml2408logplain
-rw-r--r--termdn.mli1685logplain