aboutsummaryrefslogtreecommitdiffhomepage
path: root/ltac
ModeNameSize
-rw-r--r--coretactics.ml49142logplain
-rw-r--r--evar_tactics.ml3144logplain
-rw-r--r--evar_tactics.mli883logplain
-rw-r--r--extraargs.ml412338logplain
-rw-r--r--extraargs.mli2411logplain
-rw-r--r--extratactics.ml435555logplain
-rw-r--r--extratactics.mli810logplain
-rw-r--r--g_auto.ml46347logplain
-rw-r--r--g_class.ml43590logplain
-rw-r--r--g_eqdecide.ml41158logplain
-rw-r--r--g_ltac.ml418115logplain
-rw-r--r--g_obligations.ml45178logplain
-rw-r--r--g_rewrite.ml412651logplain
-rw-r--r--ltac.mllib227logplain
-rw-r--r--profile_ltac.ml13475logplain
-rw-r--r--profile_ltac.mli2422logplain
-rw-r--r--profile_ltac_tactics.ml41349logplain
-rw-r--r--rewrite.ml82390logplain
-rw-r--r--rewrite.mli3397logplain
-rw-r--r--tacentries.ml17653logplain
-rw-r--r--tacentries.mli2738logplain
-rw-r--r--tacenv.ml4289logplain
-rw-r--r--tacenv.mli2784logplain
-rw-r--r--tacintern.ml31084logplain
-rw-r--r--tacintern.mli2012logplain
-rw-r--r--tacinterp.ml83593logplain
-rw-r--r--tacinterp.mli4406logplain
-rw-r--r--tacsubst.ml12490logplain
-rw-r--r--tacsubst.mli1108logplain
-rw-r--r--tactic_debug.ml14455logplain
-rw-r--r--tactic_debug.mli3108logplain
-rw-r--r--tactic_option.ml1962logplain
-rw-r--r--tactic_option.mli790logplain
-rw-r--r--tauto.ml9513logplain
-rw-r--r--tauto.mli0logplain