aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/ltac/tacexpr.mli
Commit message (Expand)AuthorAge
* Tactic deprecation machineryGravatar Maxime Dénès2018-07-12
* Remove reference name type.Gravatar Maxime Dénès2018-06-18
* [api] Remove Misctypes.Gravatar Emilio Jesus Gallego Arias2018-06-12
* [api] Misctypes removal: move Tactypes to proofsGravatar Emilio Jesus Gallego Arias2018-06-12
* [api] Misctypes removal: several moves:Gravatar Emilio Jesus Gallego Arias2018-06-12
* [api] Misctypes removal: multi to tactics/rewriteGravatar Emilio Jesus Gallego Arias2018-06-12
* [api] Move bullets and goals selectors to `proofs/`Gravatar Emilio Jesus Gallego Arias2018-05-01
* Strict focusing using Default Goal Selector.Gravatar Gaëtan Gilbert2018-04-29
* [api] Move some types to their proper module.Gravatar Emilio Jesus Gallego Arias2018-04-02
* [located] More work towards using CAst.tGravatar Emilio Jesus Gallego Arias2018-03-09
* Update headers following #6543.Gravatar Théo Zimmermann2018-02-27
* [ast] Improve precision of Ast location recognition in serialization.Gravatar Emilio Jesus Gallego Arias2018-02-22
* Remove deprecated option Tactic Compat Context.Gravatar Théo Zimmermann2017-12-11
* Adding support for syntax "let _ := e in e'" in Ltac.Gravatar Hugo Herbelin2017-11-04
* [general] Remove Econstr dependency from `intf`Gravatar Emilio Jesus Gallego Arias2017-10-25
* Moving the Ltac-specific part of the nametab to the Ltac plugin.Gravatar Pierre-Marie Pédrot2017-10-03
* [API] Remove `open API` in ml files in favor of `-open API` flag.Gravatar Emilio Jesus Gallego Arias2017-07-17
* Bump year in headers.Gravatar Pierre-Marie Pédrot2017-07-04
* A fix to #5414 (ident bound by ltac names now known for "match").Gravatar Hugo Herbelin2017-06-09
* Put all plugins behind an "API".Gravatar Matej Kosik2017-06-07
* Remove the Sigma (monotonous state) API.Gravatar Maxime Dénès2017-06-06
* Adding "epose", "eset", "eremember" which allow to set terms withGravatar Hugo Herbelin2017-05-30
* Adding "eassert", "eenough", "epose proof", which allow to stateGravatar Hugo Herbelin2017-05-30
* [location] Remove Loc.ghost.Gravatar Emilio Jesus Gallego Arias2017-04-25
* [location] Use located in tactics.Gravatar Emilio Jesus Gallego Arias2017-04-24
* Merge branch 'trunk' into pr379Gravatar Maxime Dénès2017-03-24
* Merge PR#432: [cleanup] Change Id.t option to Name.t in TacFunGravatar Maxime Dénès2017-03-14
* Ltac as a plugin.Gravatar Pierre-Marie Pédrot2017-02-17
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-10 09:35:51 +0000