aboutsummaryrefslogtreecommitdiff
path: root/tactics
ModeNameSize
-rw-r--r--abstract.ml8016logplain
-rw-r--r--abstract.mli1010logplain
-rw-r--r--auto.ml20296logplain
-rw-r--r--auto.mli3272logplain
-rw-r--r--autorewrite.ml10809logplain
-rw-r--r--autorewrite.mli2390logplain
-rw-r--r--btermdn.ml5604logplain
-rw-r--r--btermdn.mli1716logplain
-rw-r--r--class_tactics.ml46474logplain
-rw-r--r--class_tactics.mli2184logplain
-rw-r--r--contradiction.ml5150logplain
-rw-r--r--contradiction.mli857logplain
-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.ml18098logplain
-rw-r--r--eauto.mli1537logplain
-rw-r--r--elim.ml5578logplain
-rw-r--r--elim.mli1201logplain
-rw-r--r--elimschemes.ml5902logplain
-rw-r--r--elimschemes.mli1842logplain
-rw-r--r--eqdecide.ml9835logplain
-rw-r--r--eqdecide.mli1159logplain
-rw-r--r--eqschemes.ml42709logplain
-rw-r--r--eqschemes.mli2273logplain
-rw-r--r--equality.ml73774logplain
-rw-r--r--equality.mli6674logplain
-rw-r--r--genredexpr.ml2549logplain
-rw-r--r--hints.ml59497logplain
-rw-r--r--hints.mli11030logplain
-rw-r--r--hipattern.ml20827logplain
-rw-r--r--hipattern.mli6827logplain
-rw-r--r--ind_tables.ml7425logplain
-rw-r--r--ind_tables.mli2260logplain
-rw-r--r--inv.ml21229logplain
-rw-r--r--inv.mli1412logplain
-rw-r--r--leminv.ml10504logplain
-rw-r--r--leminv.mli960logplain
-rw-r--r--ppred.ml3251logplain
-rw-r--r--ppred.mli648logplain
-rw-r--r--redexpr.ml10014logplain
-rw-r--r--redexpr.mli1886logplain
-rw-r--r--redops.ml2704logplain
-rw-r--r--redops.mli934logplain
-rw-r--r--tacticals.ml26726logplain
-rw-r--r--tacticals.mli12532logplain
-rw-r--r--tactics.ml200029logplain
-rw-r--r--tactics.mli20033logplain
-rw-r--r--tactics.mllib219logplain
-rw-r--r--term_dnet.ml14153logplain
-rw-r--r--term_dnet.mli2796logplain