aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/ltac
ModeNameSize
-rw-r--r--Ltac.v0logplain
-rw-r--r--coretactics.ml410220logplain
-rw-r--r--evar_tactics.ml3984logplain
-rw-r--r--evar_tactics.mli932logplain
-rw-r--r--extraargs.ml413337logplain
-rw-r--r--extraargs.mli2631logplain
-rw-r--r--extratactics.ml438632logplain
-rw-r--r--extratactics.mli811logplain
-rw-r--r--g_auto.ml46875logplain
-rw-r--r--g_class.ml43895logplain
-rw-r--r--g_eqdecide.ml41159logplain
-rw-r--r--g_ltac.ml419235logplain
-rw-r--r--g_obligations.ml45539logplain
-rw-r--r--g_rewrite.ml412612logplain
-rw-r--r--g_tactic.ml427825logplain
-rw-r--r--ltac_plugin.mlpack278logplain
-rw-r--r--pltac.ml2514logplain
-rw-r--r--pltac.mli1758logplain
-rw-r--r--pptactic.ml49463logplain
-rw-r--r--pptactic.mli4015logplain
-rw-r--r--profile_ltac.ml15086logplain
-rw-r--r--profile_ltac.mli1861logplain
-rw-r--r--profile_ltac_tactics.ml41474logplain
-rw-r--r--rewrite.ml84559logplain
-rw-r--r--rewrite.mli3502logplain
-rw-r--r--tacarg.ml929logplain
-rw-r--r--tacarg.mli1177logplain
-rw-r--r--taccoerce.ml12037logplain
-rw-r--r--taccoerce.mli3323logplain
-rw-r--r--tacentries.ml19128logplain
-rw-r--r--tacentries.mli2862logplain
-rw-r--r--tacenv.ml5228logplain
-rw-r--r--tacenv.mli3136logplain
-rw-r--r--tacexpr.mli11846logplain
-rw-r--r--tacintern.ml31988logplain
-rw-r--r--tacintern.mli2028logplain
-rw-r--r--tacinterp.ml81909logplain
-rw-r--r--tacinterp.mli5339logplain
-rw-r--r--tacsubst.ml12543logplain
-rw-r--r--tacsubst.mli1108logplain
-rw-r--r--tactic_debug.ml14889logplain
-rw-r--r--tactic_debug.mli3120logplain
-rw-r--r--tactic_matching.ml15076logplain
-rw-r--r--tactic_matching.mli2223logplain
-rw-r--r--tactic_option.ml1962logplain
-rw-r--r--tactic_option.mli781logplain
-rw-r--r--tauto.ml9829logplain
-rw-r--r--tauto.mli0logplain
-rw-r--r--tauto_plugin.mlpack6logplain