aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/ltac/g_auto.ml4
Commit message (Expand)AuthorAge
* [api] Remove deprecated object from `Term`Gravatar Emilio Jesus Gallego Arias2018-05-30
* [tactics] Turn boolean locality hint parameter into a named one.Gravatar Emilio Jesus Gallego Arias2018-05-27
* Update headers following #6543.Gravatar Théo Zimmermann2018-02-27
* Change references to CAMLP4 to CAMLP5 to be more accurate since we noGravatar Jim Fehrle2018-02-17
* [plugin] Remove LocalityFixme über hack.Gravatar Emilio Jesus Gallego Arias2017-11-22
* [printing] Deprecate all printing functions accessing the global proof.Gravatar Emilio Jesus Gallego Arias2017-11-21
* Move type_uconstr to Tacinterp.Gravatar Maxime Dénès2017-08-01
* [api] Remove type equalities from API.Gravatar Emilio Jesus Gallego Arias2017-07-25
* [API] Remove `open API` in ml files in favor of `-open API` flag.Gravatar Emilio Jesus Gallego Arias2017-07-17
* plugins/ltac : avoid spurious .cmxs filesGravatar Pierre Letouzey2017-06-15
* Remove (useless) aliases from the API.Gravatar Matej Košík2017-06-10
* Put all plugins behind an "API".Gravatar Matej Kosik2017-06-07
* Remove the Sigma (monotonous state) API.Gravatar Maxime Dénès2017-06-06
* Remove unused [open] statementsGravatar Gaetan Gilbert2017-04-27
* Merge branch 'master' into econstrGravatar Pierre-Marie Pédrot2017-04-07
|\
* | Merge branch 'trunk' into pr379Gravatar Maxime Dénès2017-03-24
| * Fast path for implicit tactic solving.Gravatar Pierre-Marie Pédrot2017-03-23
|/
* Merge PR#432: [cleanup] Change Id.t option to Name.t in TacFunGravatar Maxime Dénès2017-03-14
* Merge PR#395: Allow hintdb to be parameters in a Ltac definition orGravatar Maxime Dénès2017-02-27
* Ltac as a plugin.Gravatar Pierre-Marie Pédrot2017-02-17
generated by cgit v1.2.3 (git 2.39.1) at 2024-12-11 13:34:50 +0000