aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/ltac/pptactic.mli
Commit message (Expand)AuthorAge
* [api] Remove Misctypes.Gravatar Emilio Jesus Gallego Arias2018-06-12
* [api] Misctypes removal: several moves:Gravatar Emilio Jesus Gallego Arias2018-06-12
* [notations] Split interpretation and parsing of notationsGravatar Emilio Jesus Gallego Arias2018-05-31
* [api] Move bullets and goals selectors to `proofs/`Gravatar Emilio Jesus Gallego Arias2018-05-01
* [api] Move some types to their proper module.Gravatar Emilio Jesus Gallego Arias2018-04-02
* [ssreflect] Fix module scoping problems due to packing and mli files.Gravatar Emilio Jesus Gallego Arias2018-03-10
* Update headers following #6543.Gravatar Théo Zimmermann2018-02-27
* Extending further PR#6047 (system to register printers for Ltac values).Gravatar Hugo Herbelin2017-11-24
* Setting a system to register printers for Ltac values.Gravatar Hugo Herbelin2017-11-02
* Using a specific function to register vernac printers.Gravatar Hugo Herbelin2017-11-02
* Exporting a few more printing functions.Gravatar Hugo Herbelin2017-11-02
* Moving the Ltac-specific part of the nametab to the Ltac plugin.Gravatar Pierre-Marie Pédrot2017-10-03
* Properly display the "only" prefix for selectors (bug #5760).Gravatar Guillaume Melquiond2017-09-26
* A new step of restructuration of notations.Gravatar Hugo Herbelin2017-08-29
* deprecate Pp.std_ppcmds type aliasGravatar Matej Košík2017-07-27
* [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
* Put all plugins behind an "API".Gravatar Matej Kosik2017-06-07
* [printing] Remove duplicated printing function.Gravatar Emilio Jesus Gallego Arias2017-06-01
* Merge branch 'trunk' into located_switchGravatar Emilio Jesus Gallego Arias2017-05-24
|\
| * Adding support for using grammar entries returning no value in EXTEND.Gravatar Hugo Herbelin2017-05-16
* | [location] Remove Loc.ghost.Gravatar Emilio Jesus Gallego Arias2017-04-25
|/
* Merge branch 'trunk' into pr379Gravatar Maxime Dénès2017-03-24
* [pp] Remove unused printing tagging infrastructure.Gravatar Emilio Jesus Gallego Arias2017-03-21
* Ltac as a plugin.Gravatar Pierre-Marie Pédrot2017-02-17
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-09 21:44:21 +0000