aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/ltac
ModeNameSize
-rw-r--r--Ltac.v0logplain
-rw-r--r--coretactics.ml410229logplain
-rw-r--r--evar_tactics.ml4018logplain
-rw-r--r--evar_tactics.mli941logplain
-rw-r--r--extraargs.ml413358logplain
-rw-r--r--extraargs.mli2697logplain
-rw-r--r--extratactics.ml438460logplain
-rw-r--r--extratactics.mli820logplain
-rw-r--r--g_auto.ml46896logplain
-rw-r--r--g_class.ml43868logplain
-rw-r--r--g_eqdecide.ml41167logplain
-rw-r--r--g_ltac.ml419478logplain
-rw-r--r--g_obligations.ml45637logplain
-rw-r--r--g_rewrite.ml412717logplain
-rw-r--r--g_tactic.ml427851logplain
-rw-r--r--ltac_plugin.mlpack284logplain
-rw-r--r--pltac.ml2540logplain
-rw-r--r--pltac.mli1784logplain
-rw-r--r--pptactic.ml47634logplain
-rw-r--r--pptactic.mli3845logplain
-rw-r--r--profile_ltac.ml14443logplain
-rw-r--r--profile_ltac.mli1870logplain
-rw-r--r--profile_ltac_tactics.ml41483logplain
-rw-r--r--rewrite.ml84040logplain
-rw-r--r--rewrite.mli3539logplain
-rw-r--r--tacarg.ml938logplain
-rw-r--r--tacarg.mli1186logplain
-rw-r--r--taccoerce.ml11603logplain
-rw-r--r--taccoerce.mli3310logplain
-rw-r--r--tacentries.ml18010logplain
-rw-r--r--tacentries.mli2787logplain
-rw-r--r--tacenv.ml4306logplain
-rw-r--r--tacenv.mli2781logplain
-rw-r--r--tacexpr.mli11833logplain
-rw-r--r--tacintern.ml31386logplain
-rw-r--r--tacintern.mli2068logplain
-rw-r--r--tacinterp.ml82313logplain
-rw-r--r--tacinterp.mli5142logplain
-rw-r--r--tacsubst.ml12569logplain
-rw-r--r--tacsubst.mli1117logplain
-rw-r--r--tactic_debug.ml14895logplain
-rw-r--r--tactic_debug.mli3165logplain
-rw-r--r--tactic_matching.ml15069logplain
-rw-r--r--tactic_matching.mli2227logplain
-rw-r--r--tactic_option.ml1971logplain
-rw-r--r--tactic_option.mli799logplain
-rw-r--r--tauto.ml9814logplain
-rw-r--r--tauto.mli0logplain