aboutsummaryrefslogtreecommitdiffhomepage
path: root/printing/prettyp.mli
Commit message (Expand)AuthorAge
* Swapping Context and Constr: defining declarations on constr in Constr.Gravatar Hugo Herbelin2018-06-27
* Remove reference name type.Gravatar Maxime Dénès2018-06-18
* [api] Remove Misctypes.Gravatar Emilio Jesus Gallego Arias2018-06-12
* Split off Universes functions dealing with names.Gravatar Gaëtan Gilbert2018-05-17
* [api] Rename `global_reference` to `GlobRef.t` to follow kernel style.Gravatar Emilio Jesus Gallego Arias2018-05-04
* 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
* [proof] Embed evar_map in RefinerError exception.Gravatar Emilio Jesus Gallego Arias2017-12-11
* Allow local universe renaming in Print.Gravatar Gaëtan Gilbert2017-11-25
* [printing] Deprecate all printing functions accessing the global proof.Gravatar Emilio Jesus Gallego Arias2017-11-21
* [api] Deprecate all legacy uses of Names in core.Gravatar Emilio Jesus Gallego Arias2017-11-06
* Implementing a generic mechanism for locating named objects from Coq side.Gravatar Pierre-Marie Pédrot2017-10-03
* deprecate Pp.std_ppcmds type aliasGravatar Matej Košík2017-07-27
* Bump year in headers.Gravatar Pierre-Marie Pédrot2017-07-04
* Remove unused [open] statementsGravatar Gaetan Gilbert2017-04-27
* Removing compatibility layers related to printing.Gravatar Pierre-Marie Pédrot2017-02-14
* CLEANUP: Context.{Rel,Named}.Declaration.tGravatar Matej Kosik2016-02-09
* Update copyright headers.Gravatar Maxime Dénès2016-01-20
* Update headers.Gravatar Maxime Dénès2015-01-12
* Referring to evars by names. Added a parser for evars (but parsing ofGravatar Hugo Herbelin2014-09-12
* Unifying locate code, also making it more powerful: it is now able to findGravatar Pierre-Marie Pédrot2014-07-21
* Adding a new "Locate Term" command, distinct from the raw "Locate" command.Gravatar Pierre-Marie Pédrot2014-07-21
* More complete printing of Ltac location, akin to the term-dedicated Locate co...Gravatar Pierre-Marie Pédrot2014-07-21
* Remove many superfluous 'open' indicated by ocamlc -w +33Gravatar Pierre Letouzey2014-03-05
* Merging Context and Sign.Gravatar ppedrot2013-04-29
* Modulification of nameGravatar ppedrot2012-12-18
* Modulification of identifierGravatar ppedrot2012-12-14
* Updating headers.Gravatar herbelin2012-08-08
* place all pretty-printing files in new dir printing/Gravatar letouzey2012-05-29
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-04 01:27:22 +0000