aboutsummaryrefslogtreecommitdiffhomepage
path: root/printing/printer.ml
Commit message (Expand)AuthorAge
* Split off Universes functions dealing with names.Gravatar Gaëtan Gilbert2018-05-17
* Evar maps contain econstrs.Gravatar Gaëtan Gilbert2018-04-13
* [located] Push inner locations in `reference` to a CAst.t node.Gravatar Emilio Jesus Gallego Arias2018-03-09
* Merge PR #6816: Adding mention of shelved/given-up status in Show ExistentialsGravatar Maxime Dénès2018-03-08
|\
* | Update headers following #6543.Gravatar Théo Zimmermann2018-02-27
| * Adding mention of shelved/given-up status in "Show Existentials".Gravatar Hugo Herbelin2018-02-22
|/
* Print inductive cumulativity info in About.Gravatar Gaëtan Gilbert2018-02-11
* [proof] Embed evar_map in RefinerError exception.Gravatar Emilio Jesus Gallego Arias2017-12-11
* Merge PR #1033: Universe binder improvementsGravatar Maxime Dénès2017-11-28
|\
* | [api] Remove aliases of `Evar.t`Gravatar Emilio Jesus Gallego Arias2017-11-26
| * When declaring constants/inductives use ContextSet if monomorphic.Gravatar Gaëtan Gilbert2017-11-24
| * Separate checking univ_decls and obtaining universe binder names.Gravatar Gaëtan Gilbert2017-11-24
|/
* [api] Deprecate Term destructors, move to ConstrGravatar Emilio Jesus Gallego Arias2017-11-22
* [printing] Deprecate all printing functions accessing the global proof.Gravatar Emilio Jesus Gallego Arias2017-11-21
* [proof] Attempt to deprecate some V82 parts of the proof API.Gravatar Emilio Jesus Gallego Arias2017-11-19
* [api] Another large deprecation, `Nameops`Gravatar Emilio Jesus Gallego Arias2017-11-13
* [api] Move structures deprecated in the API to the core.Gravatar Emilio Jesus Gallego Arias2017-11-06
* [api] Deprecate all legacy uses of Names in core.Gravatar Emilio Jesus Gallego Arias2017-11-06
* Finish removing Show Goal uidGravatar Gaëtan Gilbert2017-11-04
* Exporting the level-parametric printer of constr and its variants.Gravatar Hugo Herbelin2017-11-02
* Merge PR #830: Moving assert (the "Cut" rule) to new proof engineGravatar Maxime Dénès2017-08-29
|\
* | Printing goals does not evar-normalizes beforehand anymore.Gravatar Pierre-Marie Pédrot2017-08-01
* | Detyping functions are now operating on EConstr.t.Gravatar Pierre-Marie Pédrot2017-08-01
* | Merge PR #919: Remove a few useless evar-normalizations in printing code.Gravatar Maxime Dénès2017-08-01
|\ \
* | | deprecate Pp.std_ppcmds type aliasGravatar Matej Košík2017-07-27
| * | Remove a few useless evar-normalizations in printing code.Gravatar Pierre-Marie Pédrot2017-07-26
|/ /
* | Merge PR #770: [proof] Move bullets to their own module.Gravatar Maxime Dénès2017-07-19
|\ \
* | | Bump year in headers.Gravatar Pierre-Marie Pédrot2017-07-04
| | * Moving "assert" (internally "Cut") to the new proof engine.Gravatar Hugo Herbelin2017-06-25
| |/ |/|
* | Clean up universes of constants and inductivesGravatar Amin Timany2017-06-16
* | Add printing of cumulativity in inductive typesGravatar Amin Timany2017-06-16
* | Using UInfoInd for universes in inductive typesGravatar Amin Timany2017-06-16
| * [proof] Move bullets to their own module.Gravatar Emilio Jesus Gallego Arias2017-06-12
* | [proof] Deprecate redundant wrappers.Gravatar Emilio Jesus Gallego Arias2017-06-11
|/
* [emacs] [toplevel] Make emacs flag local to the toplevel.Gravatar Emilio Jesus Gallego Arias2017-06-01
* [cleanup] Unify all calls to the error function.Gravatar Emilio Jesus Gallego Arias2017-05-27
* Merge PR#481: [option] Remove support for non-synchronous options.Gravatar Maxime Dénès2017-05-25
|\
* \ Merge branch 'trunk' into located_switchGravatar Emilio Jesus Gallego Arias2017-05-24
|\ \
| | * [option] Remove support for non-synchronous options.Gravatar Emilio Jesus Gallego Arias2017-05-24
| |/
| * Merge PR#457: Adding an even more compact goal hyps mode.Gravatar Maxime Dénès2017-05-17
| |\
| | * Simplified compaction criterion + tests.Gravatar Pierre Courtieu2017-05-16
| | * Adapted to EConstr.Gravatar Pierre Courtieu2017-05-05
| * | Warning removed.Gravatar Pierre Courtieu2017-05-04
| * | labelizing argumentsGravatar Pierre Courtieu2017-05-04
| * | Adding an option "Printing Unfocused".Gravatar Pierre Courtieu2017-05-04
| | * Adding an even more compact mode for goal display.Gravatar Pierre Courtieu2017-05-03
| |/
| * Remove some unused values and typesGravatar Gaetan Gilbert2017-04-27
* | [location] Remove Loc.ghost.Gravatar Emilio Jesus Gallego Arias2017-04-25
|/
* Merge PR#441: Port Toplevel to the Stm APIGravatar Maxime Dénès2017-04-12
|\
| * [flags] Documentation and a minor tweak.Gravatar Emilio Jesus Gallego Arias2017-04-12