aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics
ModeNameSize
-rw-r--r--.cvsignore9logplain
-rw-r--r--Equality.v584logplain
-rw-r--r--Refine.v583logplain
-rw-r--r--auto.ml29906logplain
-rw-r--r--auto.mli6259logplain
-rw-r--r--autorewrite.ml3309logplain
-rw-r--r--autorewrite.mli851logplain
-rw-r--r--btermdn.ml1521logplain
-rw-r--r--btermdn.mli893logplain
-rw-r--r--contradiction.ml812logplain
-rw-r--r--contradiction.mli734logplain
-rw-r--r--dhyp.ml10746logplain
-rw-r--r--dhyp.mli1119logplain
-rw-r--r--dn.ml2915logplain
-rw-r--r--dn.mli1739logplain
-rw-r--r--doc.tex246logplain
-rw-r--r--eauto.ml412416logplain
-rw-r--r--elim.ml5314logplain
-rw-r--r--elim.mli1335logplain
-rw-r--r--eqdecide.ml45874logplain
-rw-r--r--equality.ml44084logplain
-rw-r--r--equality.mli2916logplain
-rw-r--r--extraargs.ml41266logplain
-rw-r--r--extraargs.mli919logplain
-rw-r--r--extratactics.ml47227logplain
-rw-r--r--extratactics.mli760logplain
-rw-r--r--hiddentac.ml4375logplain
-rw-r--r--hiddentac.mli3641logplain
-rw-r--r--hipattern.ml11456logplain
-rw-r--r--hipattern.mli4825logplain
-rw-r--r--inv.ml16333logplain
-rw-r--r--inv.mli1441logplain
-rw-r--r--leminv.ml10689logplain
-rw-r--r--leminv.mli440logplain
-rw-r--r--nbtermdn.ml2556logplain
-rw-r--r--nbtermdn.mli1328logplain
-rw-r--r--newtauto.ml47711logplain
-rw-r--r--refine.ml10685logplain
-rw-r--r--refine.mli657logplain
-rw-r--r--setoid_replace.ml23778logplain
-rw-r--r--setoid_replace.mli942logplain
-rw-r--r--tacinterp.ml77288logplain
-rw-r--r--tacinterp.mli3985logplain
-rw-r--r--tacticals.ml14557logplain
-rw-r--r--tacticals.mli5950logplain
-rw-r--r--tactics.ml60061logplain
-rw-r--r--tactics.mli8837logplain
-rw-r--r--tauto.ml45847logplain
-rw-r--r--termdn.ml2345logplain
-rw-r--r--termdn.mli1621logplain
-rw-r--r--wcclausenv.ml3168logplain
-rw-r--r--wcclausenv.mli1058logplain