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.ml418947logplain
-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.ml52637logplain
-rw-r--r--pptactic.mli4866logplain
-rw-r--r--profile_ltac.ml15084logplain
-rw-r--r--profile_ltac.mli1861logplain
-rw-r--r--profile_ltac_tactics.ml41471logplain
-rw-r--r--rewrite.ml84641logplain
-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.mli11841logplain
-rw-r--r--tacintern.ml32040logplain
-rw-r--r--tacintern.mli2028logplain
-rw-r--r--tacinterp.ml83054logplain
-rw-r--r--tacinterp.mli5339logplain
-rw-r--r--tacsubst.ml12609logplain
-rw-r--r--tacsubst.mli1108logplain
-rw-r--r--tactic_debug.ml15043logplain
-rw-r--r--tactic_debug.mli3120logplain
-rw-r--r--tactic_matching.ml15038logplain
-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