summaryrefslogtreecommitdiff
path: root/tactics
ModeNameSize
-rw-r--r--auto.ml40893logplain
-rw-r--r--auto.mli7961logplain
-rw-r--r--autorewrite.ml10378logplain
-rw-r--r--autorewrite.mli2083logplain
-rw-r--r--btermdn.ml4639logplain
-rw-r--r--btermdn.mli1099logplain
-rw-r--r--class_tactics.ml425970logplain
-rw-r--r--contradiction.ml2948logplain
-rw-r--r--contradiction.mli794logplain
-rw-r--r--decl_interp.ml16636logplain
-rw-r--r--decl_interp.mli824logplain
-rw-r--r--decl_proof_instr.ml46017logplain
-rw-r--r--decl_proof_instr.mli3887logplain
-rw-r--r--dhyp.ml10915logplain
-rw-r--r--dhyp.mli1129logplain
-rw-r--r--dn.ml2449logplain
-rw-r--r--dn.mli1319logplain
-rw-r--r--doc.tex246logplain
-rw-r--r--eauto.ml416640logplain
-rw-r--r--eauto.mli1320logplain
-rw-r--r--elim.ml5674logplain
-rw-r--r--elim.mli1445logplain
-rw-r--r--elimschemes.ml4962logplain
-rw-r--r--elimschemes.mli1387logplain
-rw-r--r--eqdecide.ml46340logplain
-rw-r--r--eqschemes.ml38641logplain
-rw-r--r--eqschemes.mli1934logplain
-rw-r--r--equality.ml53499logplain
-rw-r--r--equality.mli5273logplain
-rw-r--r--evar_tactics.ml2029logplain
-rw-r--r--evar_tactics.mli878logplain
-rw-r--r--extraargs.ml411743logplain
-rw-r--r--extraargs.mli2459logplain
-rw-r--r--extratactics.ml421691logplain
-rw-r--r--extratactics.mli820logplain
-rw-r--r--hiddentac.ml5386logplain
-rw-r--r--hiddentac.mli4751logplain
-rw-r--r--hightactics.mllib73logplain
-rw-r--r--hipattern.ml416293logplain
-rw-r--r--hipattern.mli6551logplain
-rw-r--r--inv.ml18655logplain
-rw-r--r--inv.mli1582logplain
-rw-r--r--leminv.ml10985logplain
-rw-r--r--leminv.mli544logplain
-rw-r--r--nbtermdn.ml4639logplain
-rw-r--r--nbtermdn.mli1577logplain
-rw-r--r--refine.ml13378logplain
-rw-r--r--refine.mli642logplain
-rw-r--r--rewrite.ml465931logplain
-rw-r--r--tacinterp.ml117849logplain
-rw-r--r--tacinterp.mli5757logplain
-rw-r--r--tactic_option.ml2202logplain
-rw-r--r--tactic_option.mli851logplain
-rw-r--r--tacticals.ml16143logplain
-rw-r--r--tacticals.mli8557logplain
-rw-r--r--tactics.ml132111logplain
-rw-r--r--tactics.mli14520logplain
-rw-r--r--tactics.mllib225logplain
-rw-r--r--tauto.ml49531logplain
-rw-r--r--termdn.ml4059logplain
-rw-r--r--termdn.mli2395logplain