summaryrefslogtreecommitdiff
path: root/tactics
ModeNameSize
-rw-r--r--auto.ml29378logplain
-rw-r--r--auto.mli6248logplain
-rw-r--r--autorewrite.ml6280logplain
-rw-r--r--autorewrite.mli1027logplain
-rw-r--r--btermdn.ml1594logplain
-rw-r--r--btermdn.mli949logplain
-rw-r--r--contradiction.ml2720logplain
-rw-r--r--contradiction.mli781logplain
-rw-r--r--dhyp.ml11425logplain
-rw-r--r--dhyp.mli1172logplain
-rw-r--r--dn.ml2965logplain
-rw-r--r--dn.mli1790logplain
-rw-r--r--doc.tex246logplain
-rw-r--r--eauto.ml413374logplain
-rw-r--r--eauto.mli1040logplain
-rw-r--r--elim.ml5648logplain
-rw-r--r--elim.mli1432logplain
-rw-r--r--eqdecide.ml46434logplain
-rw-r--r--equality.ml40475logplain
-rw-r--r--equality.mli4174logplain
-rw-r--r--evar_tactics.ml2492logplain
-rw-r--r--evar_tactics.mli841logplain
-rw-r--r--extraargs.ml43625logplain
-rw-r--r--extraargs.mli1522logplain
-rw-r--r--extratactics.ml414612logplain
-rw-r--r--extratactics.mli1281logplain
-rw-r--r--hiddentac.ml4492logplain
-rw-r--r--hiddentac.mli3650logplain
-rw-r--r--hipattern.ml411282logplain
-rw-r--r--hipattern.mli4830logplain
-rw-r--r--inv.ml19312logplain
-rw-r--r--inv.mli1497logplain
-rw-r--r--leminv.ml10675logplain
-rw-r--r--leminv.mli545logplain
-rw-r--r--nbtermdn.ml2634logplain
-rw-r--r--nbtermdn.mli1403logplain
-rw-r--r--refine.ml10948logplain
-rw-r--r--refine.mli639logplain
-rw-r--r--setoid_replace.ml75505logplain
-rw-r--r--setoid_replace.mli2708logplain
-rw-r--r--tacinterp.ml88387logplain
-rw-r--r--tacinterp.mli4550logplain
-rw-r--r--tacticals.ml15168logplain
-rw-r--r--tacticals.mli6442logplain
-rw-r--r--tactics.ml89304logplain
-rw-r--r--tactics.mli11685logplain
-rw-r--r--tauto.ml45429logplain
-rw-r--r--termdn.ml2311logplain
-rw-r--r--termdn.mli1698logplain