aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics
ModeNameSize
-rw-r--r--.cvsignore9logplain
-rw-r--r--auto.ml29943logplain
-rw-r--r--auto.mli6259logplain
-rw-r--r--autorewrite.ml3347logplain
-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.ml10784logplain
-rw-r--r--dhyp.mli1119logplain
-rw-r--r--dn.ml2915logplain
-rw-r--r--dn.mli1739logplain
-rw-r--r--doc.tex246logplain
-rw-r--r--eauto.ml412429logplain
-rw-r--r--eauto.mli840logplain
-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.ml41268logplain
-rw-r--r--extraargs.mli919logplain
-rw-r--r--extratactics.ml47227logplain
-rw-r--r--extratactics.mli760logplain
-rw-r--r--hiddentac.ml4383logplain
-rw-r--r--hiddentac.mli3661logplain
-rw-r--r--hipattern.ml11595logplain
-rw-r--r--hipattern.mli4830logplain
-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--refine.ml10685logplain
-rw-r--r--refine.mli657logplain
-rw-r--r--setoid_replace.ml23846logplain
-rw-r--r--setoid_replace.mli942logplain
-rw-r--r--tacinterp.ml78450logplain
-rw-r--r--tacinterp.mli3985logplain
-rw-r--r--tacticals.ml14659logplain
-rw-r--r--tacticals.mli6144logplain
-rw-r--r--tactics.ml60852logplain
-rw-r--r--tactics.mli8902logplain
-rw-r--r--tauto.ml46176logplain
-rw-r--r--termdn.ml2345logplain
-rw-r--r--termdn.mli1621logplain
-rw-r--r--wcclausenv.ml3168logplain
-rw-r--r--wcclausenv.mli1058logplain