summaryrefslogtreecommitdiff
path: root/plugins/ltac
ModeNameSize
-rw-r--r--Ltac.v0logplain
-rw-r--r--coretactics.ml410567logplain
-rw-r--r--evar_tactics.ml4134logplain
-rw-r--r--evar_tactics.mli1082logplain
-rw-r--r--extraargs.ml413533logplain
-rw-r--r--extraargs.mli2755logplain
-rw-r--r--extratactics.ml439486logplain
-rw-r--r--extratactics.mli961logplain
-rw-r--r--g_auto.ml47192logplain
-rw-r--r--g_class.ml44004logplain
-rw-r--r--g_eqdecide.ml41278logplain
-rw-r--r--g_ltac.ml419233logplain
-rw-r--r--g_obligations.ml45731logplain
-rw-r--r--g_rewrite.ml413164logplain
-rw-r--r--g_tactic.ml428796logplain
-rw-r--r--ltac_plugin.mlpack286logplain
-rw-r--r--pltac.ml2664logplain
-rw-r--r--pltac.mli1849logplain
-rw-r--r--pptactic.ml52946logplain
-rw-r--r--pptactic.mli5016logplain
-rw-r--r--profile_ltac.ml15912logplain
-rw-r--r--profile_ltac.mli4066logplain
-rw-r--r--profile_ltac_tactics.ml42829logplain
-rw-r--r--rewrite.ml85101logplain
-rw-r--r--rewrite.mli3672logplain
-rw-r--r--tacarg.ml1079logplain
-rw-r--r--tacarg.mli1327logplain
-rw-r--r--taccoerce.ml14591logplain
-rw-r--r--taccoerce.mli4154logplain
-rw-r--r--tacentries.ml24649logplain
-rw-r--r--tacentries.mli3454logplain
-rw-r--r--tacenv.ml5378logplain
-rw-r--r--tacenv.mli3282logplain
-rw-r--r--tacexpr.ml11921logplain
-rw-r--r--tacexpr.mli11921logplain
-rw-r--r--tacintern.ml32227logplain
-rw-r--r--tacintern.mli2158logplain
-rw-r--r--tacinterp.ml79898logplain
-rw-r--r--tacinterp.mli5075logplain
-rw-r--r--tacsubst.ml12785logplain
-rw-r--r--tacsubst.mli1258logplain
-rw-r--r--tactic_debug.ml15135logplain
-rw-r--r--tactic_debug.mli3270logplain
-rw-r--r--tactic_matching.ml15198logplain
-rw-r--r--tactic_matching.mli2372logplain
-rw-r--r--tactic_option.ml2112logplain
-rw-r--r--tactic_option.mli931logplain
-rw-r--r--tauto.ml9472logplain
-rw-r--r--tauto.mli0logplain
-rw-r--r--tauto_plugin.mlpack6logplain
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-17 12:21:15 +0000