aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics
ModeNameSize
-rw-r--r--auto.ml53299logplain
-rw-r--r--auto.mli9317logplain
-rw-r--r--autorewrite.ml10448logplain
-rw-r--r--autorewrite.mli2102logplain
-rw-r--r--btermdn.ml5029logplain
-rw-r--r--btermdn.mli1569logplain
-rw-r--r--class_tactics.ml25890logplain
-rw-r--r--class_tactics.mli1149logplain
-rw-r--r--contradiction.ml4200logplain
-rw-r--r--contradiction.mli705logplain
-rw-r--r--dn.ml2517logplain
-rw-r--r--dn.mli1221logplain
-rw-r--r--doc.tex246logplain
-rw-r--r--eauto.ml420481logplain
-rw-r--r--eauto.mli1274logplain
-rw-r--r--elim.ml6045logplain
-rw-r--r--elim.mli1504logplain
-rw-r--r--elimschemes.ml4584logplain
-rw-r--r--elimschemes.mli1378logplain
-rw-r--r--eqdecide.ml7006logplain
-rw-r--r--eqdecide.mli1007logplain
-rw-r--r--eqschemes.ml38364logplain
-rw-r--r--eqschemes.mli1878logplain
-rw-r--r--equality.ml64244logplain
-rw-r--r--equality.mli5862logplain
-rw-r--r--evar_tactics.ml2217logplain
-rw-r--r--evar_tactics.mli784logplain
-rw-r--r--extraargs.ml412245logplain
-rw-r--r--extraargs.mli2589logplain
-rw-r--r--extratactics.ml430121logplain
-rw-r--r--extratactics.mli799logplain
-rw-r--r--g_class.ml42667logplain
-rw-r--r--g_eqdecide.ml41129logplain
-rw-r--r--g_rewrite.ml412949logplain
-rw-r--r--geninterp.ml1195logplain
-rw-r--r--geninterp.mli1067logplain
-rw-r--r--hightactics.mllib95logplain
-rw-r--r--hipattern.ml417498logplain
-rw-r--r--hipattern.mli6552logplain
-rw-r--r--inv.ml20097logplain
-rw-r--r--inv.mli1603logplain
-rw-r--r--leminv.ml10289logplain
-rw-r--r--leminv.mli1091logplain
-rw-r--r--rewrite.ml67221logplain
-rw-r--r--rewrite.mli2745logplain
-rw-r--r--taccoerce.ml8459logplain
-rw-r--r--taccoerce.mli2772logplain
-rw-r--r--tacenv.ml7887logplain
-rw-r--r--tacenv.mli2014logplain
-rw-r--r--tacintern.ml31678logplain
-rw-r--r--tacintern.mli2250logplain
-rw-r--r--tacinterp.ml82227logplain
-rw-r--r--tacinterp.mli4161logplain
-rw-r--r--tacsubst.ml14039logplain
-rw-r--r--tacsubst.mli1108logplain
-rw-r--r--tacticMatching.ml14071logplain
-rw-r--r--tacticMatching.mli2134logplain
-rw-r--r--tactic_option.ml1962logplain
-rw-r--r--tactic_option.mli790logplain
-rw-r--r--tacticals.ml24386logplain
-rw-r--r--tacticals.mli12562logplain
-rw-r--r--tactics.ml144697logplain
-rw-r--r--tactics.mli16104logplain
-rw-r--r--tactics.mllib226logplain
-rw-r--r--tauto.ml412348logplain