aboutsummaryrefslogtreecommitdiff
path: root/plugins/ltac/g_auto.ml4
AgeCommit message (Expand)Author
2018-10-15Port remaining EXTEND ml4 files to coqpp.Pierre-Marie Pédrot
2018-10-15Plug ARGUMENT EXTEND into the argument extension API.Pierre-Marie Pédrot
2018-10-15Deprecating the RAW_TYPED and GLOB_TYPED stanzas of the ARGUMENT EXTEND macro.Pierre-Marie Pédrot
2018-06-18Remove reference name type.Maxime Dénès
2018-05-30[api] Remove deprecated object from `Term`Emilio Jesus Gallego Arias
2018-05-27[tactics] Turn boolean locality hint parameter into a named one.Emilio Jesus Gallego Arias
2018-02-27Update headers following #6543.Théo Zimmermann
2018-02-17Change references to CAMLP4 to CAMLP5 to be more accurate since we noJim Fehrle
2017-11-22[plugin] Remove LocalityFixme über hack.Emilio Jesus Gallego Arias
2017-11-21[printing] Deprecate all printing functions accessing the global proof.Emilio Jesus Gallego Arias
2017-08-01Move type_uconstr to Tacinterp.Maxime Dénès
2017-07-25[api] Remove type equalities from API.Emilio Jesus Gallego Arias
2017-07-17[API] Remove `open API` in ml files in favor of `-open API` flag.Emilio Jesus Gallego Arias
2017-06-15plugins/ltac : avoid spurious .cmxs filesPierre Letouzey
2017-06-10Remove (useless) aliases from the API.Matej Košík
2017-06-07Put all plugins behind an "API".Matej Kosik
2017-06-06Remove the Sigma (monotonous state) API.Maxime Dénès
2017-04-27Remove unused [open] statementsGaetan Gilbert
2017-04-07Merge branch 'master' into econstrPierre-Marie Pédrot
2017-03-24Merge branch 'trunk' into pr379Maxime Dénès
2017-03-23Fast path for implicit tactic solving.Pierre-Marie Pédrot
2017-03-14Merge PR#432: [cleanup] Change Id.t option to Name.t in TacFunMaxime Dénès
2017-02-27Merge PR#395: Allow hintdb to be parameters in a Ltac definition orMaxime Dénès
2017-02-17Ltac as a plugin.Pierre-Marie Pédrot
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-12 03:51:32 +0000