aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/ltac
ModeNameSize
-rw-r--r--Ltac.v0logplain
-rw-r--r--coretactics.ml410183logplain
-rw-r--r--evar_tactics.ml3984logplain
-rw-r--r--evar_tactics.mli932logplain
-rw-r--r--extraargs.ml413383logplain
-rw-r--r--extraargs.mli2605logplain
-rw-r--r--extratactics.ml439079logplain
-rw-r--r--extratactics.mli811logplain
-rw-r--r--g_auto.ml47042logplain
-rw-r--r--g_class.ml43854logplain
-rw-r--r--g_eqdecide.ml41116logplain
-rw-r--r--g_ltac.ml419041logplain
-rw-r--r--g_obligations.ml45579logplain
-rw-r--r--g_rewrite.ml413014logplain
-rw-r--r--g_tactic.ml428538logplain
-rw-r--r--ltac_plugin.mlpack278logplain
-rw-r--r--pltac.ml2514logplain
-rw-r--r--pltac.mli1709logplain
-rw-r--r--pptactic.ml52759logplain
-rw-r--r--pptactic.mli4866logplain
-rw-r--r--profile_ltac.ml15762logplain
-rw-r--r--profile_ltac.mli3916logplain
-rw-r--r--profile_ltac_tactics.ml42679logplain
-rw-r--r--rewrite.ml84823logplain
-rw-r--r--rewrite.mli3522logplain
-rw-r--r--tacarg.ml929logplain
-rw-r--r--tacarg.mli1177logplain
-rw-r--r--taccoerce.ml11555logplain
-rw-r--r--taccoerce.mli3245logplain
-rw-r--r--tacentries.ml19120logplain
-rw-r--r--tacentries.mli2862logplain
-rw-r--r--tacenv.ml5228logplain
-rw-r--r--tacenv.mli3136logplain
-rw-r--r--tacexpr.mli11783logplain
-rw-r--r--tacintern.ml32164logplain
-rw-r--r--tacintern.mli2008logplain
-rw-r--r--tacinterp.ml83048logplain
-rw-r--r--tacinterp.mli5309logplain
-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.ml15048logplain
-rw-r--r--tactic_matching.mli2223logplain
-rw-r--r--tactic_option.ml1962logplain
-rw-r--r--tactic_option.mli781logplain
-rw-r--r--tauto.ml9830logplain
-rw-r--r--tauto.mli0logplain
-rw-r--r--tauto_plugin.mlpack6logplain