aboutsummaryrefslogtreecommitdiffhomepage
path: root/ltac
ModeNameSize
-rw-r--r--coretactics.ml49368logplain
-rw-r--r--evar_tactics.ml3241logplain
-rw-r--r--evar_tactics.mli883logplain
-rw-r--r--extraargs.ml412744logplain
-rw-r--r--extraargs.mli2554logplain
-rw-r--r--extratactics.ml437603logplain
-rw-r--r--extratactics.mli810logplain
-rw-r--r--g_auto.ml46620logplain
-rw-r--r--g_class.ml43446logplain
-rw-r--r--g_eqdecide.ml41198logplain
-rw-r--r--g_ltac.ml419090logplain
-rw-r--r--g_obligations.ml45638logplain
-rw-r--r--g_rewrite.ml412614logplain
-rw-r--r--g_tactic.ml425125logplain
-rw-r--r--ltac.mllib284logplain
-rw-r--r--pltac.ml2525logplain
-rw-r--r--pltac.mli1758logplain
-rw-r--r--pptactic.ml50906logplain
-rw-r--r--pptactic.mli2191logplain
-rw-r--r--pptacticsig.mli2771logplain
-rw-r--r--profile_ltac.ml14540logplain
-rw-r--r--profile_ltac.mli1860logplain
-rw-r--r--profile_ltac_tactics.ml41474logplain
-rw-r--r--rewrite.ml86293logplain
-rw-r--r--rewrite.mli3545logplain
-rw-r--r--tacarg.ml929logplain
-rw-r--r--tacarg.mli1177logplain
-rw-r--r--taccoerce.ml11356logplain
-rw-r--r--taccoerce.mli3125logplain
-rw-r--r--tacentries.ml17874logplain
-rw-r--r--tacentries.mli2735logplain
-rw-r--r--tacenv.ml4286logplain
-rw-r--r--tacenv.mli2784logplain
-rw-r--r--tacexpr.mli11828logplain
-rw-r--r--tacintern.ml31241logplain
-rw-r--r--tacintern.mli2012logplain
-rw-r--r--tacinterp.ml84327logplain
-rw-r--r--tacinterp.mli4406logplain
-rw-r--r--tacsubst.ml12499logplain
-rw-r--r--tacsubst.mli1108logplain
-rw-r--r--tactic_debug.ml14501logplain
-rw-r--r--tactic_debug.mli3108logplain
-rw-r--r--tactic_matching.ml15128logplain
-rw-r--r--tactic_matching.mli2199logplain
-rw-r--r--tactic_option.ml1962logplain
-rw-r--r--tactic_option.mli790logplain
-rw-r--r--tauto.ml10264logplain
-rw-r--r--tauto.mli0logplain