aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics
ModeNameSize
-rw-r--r--.cvsignore9logplain
-rw-r--r--Equality.v584logplain
-rw-r--r--Refine.v583logplain
-rw-r--r--auto.ml29394logplain
-rw-r--r--auto.mli6017logplain
-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.ml9594logplain
-rw-r--r--dhyp.mli1015logplain
-rw-r--r--dn.ml2915logplain
-rw-r--r--dn.mli1739logplain
-rw-r--r--doc.tex246logplain
-rw-r--r--eauto.ml411851logplain
-rw-r--r--elim.ml6240logplain
-rw-r--r--elim.mli1646logplain
-rw-r--r--eqdecide.ml46124logplain
-rw-r--r--equality.ml41521logplain
-rw-r--r--equality.mli2976logplain
-rw-r--r--extraargs.ml42843logplain
-rw-r--r--extraargs.mli898logplain
-rw-r--r--extratactics.ml46773logplain
-rw-r--r--extratactics.mli760logplain
-rw-r--r--hiddentac.ml4389logplain
-rw-r--r--hiddentac.mli3550logplain
-rw-r--r--hipattern.ml6024logplain
-rw-r--r--hipattern.mli3331logplain
-rw-r--r--inv.ml16896logplain
-rw-r--r--inv.mli1441logplain
-rw-r--r--leminv.ml10672logplain
-rw-r--r--leminv.mli423logplain
-rw-r--r--nbtermdn.ml2556logplain
-rw-r--r--nbtermdn.mli1328logplain
-rw-r--r--refine.ml10713logplain
-rw-r--r--refine.mli657logplain
-rw-r--r--setoid_replace.ml23590logplain
-rw-r--r--setoid_replace.mli935logplain
-rw-r--r--tacinterp.ml63762logplain
-rw-r--r--tacinterp.mli3693logplain
-rw-r--r--tacticals.ml14489logplain
-rw-r--r--tacticals.mli5949logplain
-rw-r--r--tactics.ml58144logplain
-rw-r--r--tactics.mli8577logplain
-rw-r--r--tauto.ml44754logplain
-rw-r--r--termdn.ml2345logplain
-rw-r--r--termdn.mli1621logplain
-rw-r--r--wcclausenv.ml5493logplain
-rw-r--r--wcclausenv.mli1395logplain