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.ml413395logplain
-rw-r--r--extraargs.mli2631logplain
-rw-r--r--extratactics.ml438396logplain
-rw-r--r--extratactics.mli811logplain
-rw-r--r--g_auto.ml47085logplain
-rw-r--r--g_class.ml43897logplain
-rw-r--r--g_eqdecide.ml41159logplain
-rw-r--r--g_ltac.ml419431logplain
-rw-r--r--g_obligations.ml45621logplain
-rw-r--r--g_rewrite.ml413057logplain
-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.ml52792logplain
-rw-r--r--pptactic.mli4866logplain
-rw-r--r--profile_ltac.ml15086logplain
-rw-r--r--profile_ltac.mli1861logplain
-rw-r--r--profile_ltac_tactics.ml41474logplain
-rw-r--r--rewrite.ml84590logplain
-rw-r--r--rewrite.mli3522logplain
-rw-r--r--tacarg.ml929logplain
-rw-r--r--tacarg.mli1177logplain
-rw-r--r--taccoerce.ml12054logplain
-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.mli11848logplain
-rw-r--r--tacintern.ml32044logplain
-rw-r--r--tacintern.mli2028logplain
-rw-r--r--tacinterp.ml83046logplain
-rw-r--r--tacinterp.mli5339logplain
-rw-r--r--tacsubst.ml12613logplain
-rw-r--r--tacsubst.mli1108logplain
-rw-r--r--tactic_debug.ml15043logplain
-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