aboutsummaryrefslogtreecommitdiff
path: root/tactics
ModeNameSize
-rw-r--r--abstract.ml7828logplain
-rw-r--r--abstract.mli1312logplain
-rw-r--r--auto.ml20416logplain
-rw-r--r--auto.mli3252logplain
-rw-r--r--autorewrite.ml11005logplain
-rw-r--r--autorewrite.mli2359logplain
-rw-r--r--btermdn.ml5686logplain
-rw-r--r--btermdn.mli1716logplain
-rw-r--r--class_tactics.ml46831logplain
-rw-r--r--class_tactics.mli2490logplain
-rw-r--r--contradiction.ml5305logplain
-rw-r--r--contradiction.mli857logplain
-rw-r--r--declare.ml25466logplain
-rw-r--r--declare.mli3962logplain
-rw-r--r--dn.ml2513logplain
-rw-r--r--dn.mli1166logplain
-rw-r--r--dnet.ml10325logplain
-rw-r--r--dnet.mli4665logplain
-rw-r--r--doc.tex246logplain
-rw-r--r--dune145logplain
-rw-r--r--eauto.ml18117logplain
-rw-r--r--eauto.mli1537logplain
-rw-r--r--elim.ml5638logplain
-rw-r--r--elim.mli1201logplain
-rw-r--r--elimschemes.ml6788logplain
-rw-r--r--elimschemes.mli2081logplain
-rw-r--r--eqdecide.ml9972logplain
-rw-r--r--eqdecide.mli1159logplain
-rw-r--r--eqschemes.ml43635logplain
-rw-r--r--eqschemes.mli2247logplain
-rw-r--r--equality.ml74314logplain
-rw-r--r--equality.mli6675logplain
-rw-r--r--genredexpr.ml2549logplain
-rw-r--r--hints.ml60057logplain
-rw-r--r--hints.mli11008logplain
-rw-r--r--hipattern.ml21217logplain
-rw-r--r--hipattern.mli6849logplain
-rw-r--r--ind_tables.ml7530logplain
-rw-r--r--ind_tables.mli2281logplain
-rw-r--r--inv.ml21268logplain
-rw-r--r--inv.mli1412logplain
-rw-r--r--leminv.ml10750logplain
-rw-r--r--leminv.mli960logplain
-rw-r--r--ppred.ml3251logplain
-rw-r--r--ppred.mli512logplain
-rw-r--r--redexpr.ml10087logplain
-rw-r--r--redexpr.mli1886logplain
-rw-r--r--redops.ml2693logplain
-rw-r--r--redops.mli934logplain
-rw-r--r--tacticals.ml26398logplain
-rw-r--r--tacticals.mli12077logplain
-rw-r--r--tactics.ml202953logplain
-rw-r--r--tactics.mli20125logplain
-rw-r--r--tactics.mllib227logplain
-rw-r--r--term_dnet.ml14164logplain
-rw-r--r--term_dnet.mli2796logplain