aboutsummaryrefslogtreecommitdiff
path: root/tactics
ModeNameSize
-rw-r--r--abstract.ml4293logplain
-rw-r--r--abstract.mli1335logplain
-rw-r--r--auto.ml19682logplain
-rw-r--r--auto.mli3108logplain
-rw-r--r--autorewrite.ml11133logplain
-rw-r--r--autorewrite.mli2160logplain
-rw-r--r--btermdn.ml6600logplain
-rw-r--r--btermdn.mli1721logplain
-rw-r--r--cbn.ml31405logplain
-rw-r--r--cbn.mli1073logplain
-rw-r--r--class_tactics.ml46813logplain
-rw-r--r--class_tactics.mli2497logplain
-rw-r--r--contradiction.ml5558logplain
-rw-r--r--contradiction.mli857logplain
-rw-r--r--declareScheme.ml1796logplain
-rw-r--r--declareScheme.mli865logplain
-rw-r--r--declareUctx.ml1591logplain
-rw-r--r--declareUctx.mli746logplain
-rw-r--r--dn.ml2544logplain
-rw-r--r--dn.mli1165logplain
-rw-r--r--dnet.ml10997logplain
-rw-r--r--dnet.mli4665logplain
-rw-r--r--doc.tex246logplain
-rw-r--r--dune150logplain
-rw-r--r--eauto.ml17275logplain
-rw-r--r--eauto.mli1501logplain
-rw-r--r--elim.ml7728logplain
-rw-r--r--elim.mli1137logplain
-rw-r--r--elimschemes.ml6671logplain
-rw-r--r--elimschemes.mli1891logplain
-rw-r--r--eqdecide.ml10144logplain
-rw-r--r--eqdecide.mli1159logplain
-rw-r--r--eqschemes.ml44686logplain
-rw-r--r--eqschemes.mli2205logplain
-rw-r--r--equality.ml76688logplain
-rw-r--r--equality.mli6774logplain
-rw-r--r--genredexpr.ml2606logplain
-rw-r--r--hints.ml61165logplain
-rw-r--r--hints.mli8986logplain
-rw-r--r--hipattern.ml21565logplain
-rw-r--r--hipattern.mli6861logplain
-rw-r--r--ind_tables.ml8253logplain
-rw-r--r--ind_tables.mli2809logplain
-rw-r--r--inv.ml21750logplain
-rw-r--r--inv.mli1412logplain
-rw-r--r--ppred.ml3251logplain
-rw-r--r--ppred.mli699logplain
-rw-r--r--redexpr.ml12991logplain
-rw-r--r--redexpr.mli2164logplain
-rw-r--r--redops.ml2693logplain
-rw-r--r--redops.mli934logplain
-rw-r--r--tacticals.ml30924logplain
-rw-r--r--tacticals.mli11956logplain
-rw-r--r--tactics.ml210852logplain
-rw-r--r--tactics.mli20474logplain
-rw-r--r--tactics.mllib242logplain
-rw-r--r--term_dnet.ml15673logplain
-rw-r--r--term_dnet.mli2796logplain