aboutsummaryrefslogtreecommitdiff
path: root/tactics
ModeNameSize
-rw-r--r--abstract.ml4201logplain
-rw-r--r--abstract.mli1335logplain
-rw-r--r--auto.ml20912logplain
-rw-r--r--auto.mli3252logplain
-rw-r--r--autorewrite.ml11401logplain
-rw-r--r--autorewrite.mli2429logplain
-rw-r--r--btermdn.ml5776logplain
-rw-r--r--btermdn.mli1716logplain
-rw-r--r--class_tactics.ml48503logplain
-rw-r--r--class_tactics.mli2657logplain
-rw-r--r--contradiction.ml5336logplain
-rw-r--r--contradiction.mli857logplain
-rw-r--r--declareScheme.ml1748logplain
-rw-r--r--declareScheme.mli824logplain
-rw-r--r--declareUctx.ml1572logplain
-rw-r--r--declareUctx.mli746logplain
-rw-r--r--dn.ml2758logplain
-rw-r--r--dn.mli1166logplain
-rw-r--r--dnet.ml10997logplain
-rw-r--r--dnet.mli4665logplain
-rw-r--r--doc.tex246logplain
-rw-r--r--dune145logplain
-rw-r--r--eauto.ml19350logplain
-rw-r--r--eauto.mli1541logplain
-rw-r--r--elim.ml5612logplain
-rw-r--r--elim.mli1201logplain
-rw-r--r--elimschemes.ml6671logplain
-rw-r--r--elimschemes.mli1891logplain
-rw-r--r--eqdecide.ml10048logplain
-rw-r--r--eqdecide.mli1159logplain
-rw-r--r--eqschemes.ml44065logplain
-rw-r--r--eqschemes.mli2205logplain
-rw-r--r--equality.ml75834logplain
-rw-r--r--equality.mli6748logplain
-rw-r--r--genredexpr.ml2549logplain
-rw-r--r--hints.ml56873logplain
-rw-r--r--hints.mli10696logplain
-rw-r--r--hipattern.ml21437logplain
-rw-r--r--hipattern.mli6861logplain
-rw-r--r--ind_tables.ml8250logplain
-rw-r--r--ind_tables.mli2809logplain
-rw-r--r--inv.ml21554logplain
-rw-r--r--inv.mli1412logplain
-rw-r--r--ppred.ml3251logplain
-rw-r--r--ppred.mli512logplain
-rw-r--r--redexpr.ml9935logplain
-rw-r--r--redexpr.mli1886logplain
-rw-r--r--redops.ml2693logplain
-rw-r--r--redops.mli934logplain
-rw-r--r--tacticals.ml26544logplain
-rw-r--r--tacticals.mli12204logplain
-rw-r--r--tactics.ml211944logplain
-rw-r--r--tactics.mli20397logplain
-rw-r--r--tactics.mllib238logplain
-rw-r--r--term_dnet.ml14754logplain
-rw-r--r--term_dnet.mli2796logplain