aboutsummaryrefslogtreecommitdiffhomepage
path: root/printing/printmod.ml
Commit message (Expand)AuthorAge
* [api] Also deprecate constructors of Decl_kinds.Gravatar Emilio Jesus Gallego Arias2017-12-23
* Merge PR #6244: [lib] [api] Introduce record for `object_prefix`Gravatar Maxime Dénès2017-11-30
|\
| * [lib] [api] Introduce record for `object_prefix`Gravatar Emilio Jesus Gallego Arias2017-11-29
* | 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] 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
* Efficient fresh name generation relying on sets.Gravatar Pierre-Marie Pédrot2017-09-28
* Removing template polymorphism for definitions.Gravatar Pierre-Marie Pédrot2017-07-26
* The only abstraction-breaking function in Univ is now AUContext.instance.Gravatar Pierre-Marie Pédrot2017-07-13
* Safe API for accessing universe constraints of global references.Gravatar Pierre-Marie Pédrot2017-07-11
* Bump year in headers.Gravatar Pierre-Marie Pédrot2017-07-04
* 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
* [option] Remove support for non-synchronous options.Gravatar Emilio Jesus Gallego Arias2017-05-24
* Merge branch 'trunk' into pr379Gravatar Maxime Dénès2017-03-24
|\
| * [pp] Move terminal-specific tagging to the toplevel.Gravatar Emilio Jesus Gallego Arias2017-03-21
| * [pp] Prepare for serialization, remove opaque glue.Gravatar Emilio Jesus Gallego Arias2017-03-21
| * [pp] Replace `Pp.Tag` by `Ppstyle.tag` = `string list`Gravatar Emilio Jesus Gallego Arias2017-03-21
* | Introducing contexts parameterized by the inner term type.Gravatar Pierre-Marie Pédrot2017-02-14
|/
* Fix bug #4661: Cannot mask the absolute name.Gravatar Pierre-Marie Pédrot2016-10-01
* errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib mod...Gravatar Pierre Letouzey2016-07-03
* Removing dead code and unused opens.Gravatar Pierre-Marie Pédrot2016-05-08
* Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-01-21
|\
| * Update copyright headers.Gravatar Maxime Dénès2016-01-20
* | mergeGravatar Matej Kosik2016-01-11
|\ \
| * | CLEANUP: kernel/context.ml{,i}Gravatar Matej Kosik2016-01-11
* | | Do not compose "str" and "to_string" whenever possible.Gravatar Guillaume Melquiond2015-12-22
|/ /
* / Moving extended_rel_vect/extended_rel_list to the kernel.Gravatar Hugo Herbelin2015-12-05
|/
* Univs: local names handling.Gravatar Matthieu Sozeau2015-10-28
* Printing of @{} instances for polymorphic references in Print and About.Gravatar Matthieu Sozeau2015-10-28
* Univs: fix printing bug #3797.Gravatar Matthieu Sozeau2015-10-05
* Fixing bug #2169:Gravatar Pierre-Marie Pédrot2015-07-27
* Update headers.Gravatar Maxime Dénès2015-01-12
* Declarations.mli refactoring: module_type_body = module_bodyGravatar Pierre Letouzey2015-01-11
* Setting printing flags on the printing of mutual inductives.Gravatar Pierre-Marie Pédrot2014-11-20
* Moving mutual inductive printing from Printer to Printmod.Gravatar Pierre-Marie Pédrot2014-11-20
* Adding rich-printing facilities to Printmod.Gravatar Pierre-Marie Pédrot2014-11-19
* Referring to evars by names. Added a parser for evars (but parsing ofGravatar Hugo Herbelin2014-09-12
* Print [Variant] types with the keyword [Variant].Gravatar Arnaud Spiwack2014-09-04
* "allows to", like "allowing to", is improperGravatar Jason Gross2014-08-25
* Print universes in module printingGravatar Matthieu Sozeau2014-05-06
* Initial work on reintroducing old-style polymorphism for compatibility (the s...Gravatar Matthieu Sozeau2014-05-06
* This commit adds full universe polymorphism and fast projections to Coq.Gravatar Matthieu Sozeau2014-05-06
* Remove many superfluous 'open' indicated by ocamlc -w +33Gravatar Pierre Letouzey2014-03-05
* Lazyconstr -> OpaqueproofGravatar Enrico Tassi2014-02-26
* Turn many List.assoc into List.assoc_fGravatar letouzey2013-10-24
* Declarations.mli: reorganization of modular structuresGravatar letouzey2013-08-20
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-27 22:38:45 +0000