aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/ltac
ModeNameSize
-rw-r--r--Ltac.v0logplain
-rw-r--r--coretactics.ml410486logplain
-rw-r--r--evar_tactics.ml4065logplain
-rw-r--r--evar_tactics.mli1082logplain
-rw-r--r--extraargs.ml413511logplain
-rw-r--r--extraargs.mli2764logplain
-rw-r--r--extratactics.ml437105logplain
-rw-r--r--extratactics.mli961logplain
-rw-r--r--g_auto.ml47200logplain
-rw-r--r--g_class.ml44004logplain
-rw-r--r--g_eqdecide.ml41278logplain
-rw-r--r--g_ltac.ml419196logplain
-rw-r--r--g_obligations.ml45717logplain
-rw-r--r--g_rewrite.ml413160logplain
-rw-r--r--g_tactic.ml428838logplain
-rw-r--r--ltac_plugin.mlpack286logplain
-rw-r--r--pltac.ml2664logplain
-rw-r--r--pltac.mli1874logplain
-rw-r--r--pptactic.ml53059logplain
-rw-r--r--pptactic.mli5008logplain
-rw-r--r--profile_ltac.ml15912logplain
-rw-r--r--profile_ltac.mli4066logplain
-rw-r--r--profile_ltac_tactics.ml42829logplain
-rw-r--r--rewrite.ml84985logplain
-rw-r--r--rewrite.mli3671logplain
-rw-r--r--tacarg.ml1416logplain
-rw-r--r--tacarg.mli2256logplain
-rw-r--r--taccoerce.ml14621logplain
-rw-r--r--taccoerce.mli4150logplain
-rw-r--r--tacentries.ml24605logplain
-rw-r--r--tacentries.mli3451logplain
-rw-r--r--tacenv.ml5378logplain
-rw-r--r--tacenv.mli3286logplain
-rw-r--r--tacexpr.ml12191logplain
-rw-r--r--tacexpr.mli12191logplain
-rw-r--r--tacintern.ml32391logplain
-rw-r--r--tacintern.mli2157logplain
-rw-r--r--tacinterp.ml79893logplain
-rw-r--r--tacinterp.mli5080logplain
-rw-r--r--tacsubst.ml12801logplain
-rw-r--r--tacsubst.mli1257logplain
-rw-r--r--tactic_debug.ml15003logplain
-rw-r--r--tactic_debug.mli3260logplain
-rw-r--r--tactic_matching.ml15211logplain
-rw-r--r--tactic_matching.mli2372logplain
-rw-r--r--tactic_option.ml2112logplain
-rw-r--r--tactic_option.mli931logplain
-rw-r--r--tauto.ml9469logplain
-rw-r--r--tauto.mli0logplain
-rw-r--r--tauto_plugin.mlpack6logplain