aboutsummaryrefslogtreecommitdiffhomepage
path: root/printing/printmod.ml
Commit message (Expand)AuthorAge
* 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
* Declaremods: major refactoring, stop duplicating libobjects in modulesGravatar letouzey2013-07-17
* Printmod: handle more examples thanks to better nametab useGravatar letouzey2013-03-21
* Printmod: fresh fake namespaces for non-visible modules (fix #2668, #2983)Gravatar letouzey2013-03-21
* Declaremods: a few syntactic improvementsGravatar letouzey2013-03-13
* Restrict (try...with...) to avoid catching critical exn (part 13)Gravatar letouzey2013-03-13
* Restrict (try...with...) to avoid catching critical exn (part 5)Gravatar letouzey2013-03-13
* kernel/declarations becomes a pure mliGravatar letouzey2013-02-26
* Names: shortcuts for building {kn, constant, mind} with empty sectionsGravatar letouzey2013-02-26
* Dir_path --> DirPathGravatar letouzey2013-02-19
* Minor code cleanups, especially take advantage of Dir_path.is_emptyGravatar letouzey2013-02-18
* Uniformization of the "anomaly" command.Gravatar ppedrot2013-01-28
* Modulification of mod_bound_idGravatar ppedrot2012-12-18
* Modulification of LabelGravatar ppedrot2012-12-18
* Modulification of dir_pathGravatar ppedrot2012-12-14
* Modulification of identifierGravatar ppedrot2012-12-14
* Updating headers.Gravatar herbelin2012-08-08
* Fixing bug #2809 (anomaly when printing a module with notations due toGravatar herbelin2012-06-20
* place all pretty-printing files in new dir printing/Gravatar letouzey2012-05-29