index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
printing
/
printmod.ml
Commit message (
Expand
)
Author
Age
*
Univs: local names handling.
Matthieu Sozeau
2015-10-28
*
Printing of @{} instances for polymorphic references in Print and About.
Matthieu Sozeau
2015-10-28
*
Univs: fix printing bug #3797.
Matthieu Sozeau
2015-10-05
*
Fixing bug #2169:
Pierre-Marie Pédrot
2015-07-27
*
Update headers.
Maxime Dénès
2015-01-12
*
Declarations.mli refactoring: module_type_body = module_body
Pierre Letouzey
2015-01-11
*
Setting printing flags on the printing of mutual inductives.
Pierre-Marie Pédrot
2014-11-20
*
Moving mutual inductive printing from Printer to Printmod.
Pierre-Marie Pédrot
2014-11-20
*
Adding rich-printing facilities to Printmod.
Pierre-Marie Pédrot
2014-11-19
*
Referring to evars by names. Added a parser for evars (but parsing of
Hugo Herbelin
2014-09-12
*
Print [Variant] types with the keyword [Variant].
Arnaud Spiwack
2014-09-04
*
"allows to", like "allowing to", is improper
Jason Gross
2014-08-25
*
Print universes in module printing
Matthieu Sozeau
2014-05-06
*
Initial work on reintroducing old-style polymorphism for compatibility (the s...
Matthieu Sozeau
2014-05-06
*
This commit adds full universe polymorphism and fast projections to Coq.
Matthieu Sozeau
2014-05-06
*
Remove many superfluous 'open' indicated by ocamlc -w +33
Pierre Letouzey
2014-03-05
*
Lazyconstr -> Opaqueproof
Enrico Tassi
2014-02-26
*
Turn many List.assoc into List.assoc_f
letouzey
2013-10-24
*
Declarations.mli: reorganization of modular structures
letouzey
2013-08-20
*
Declaremods: major refactoring, stop duplicating libobjects in modules
letouzey
2013-07-17
*
Printmod: handle more examples thanks to better nametab use
letouzey
2013-03-21
*
Printmod: fresh fake namespaces for non-visible modules (fix #2668, #2983)
letouzey
2013-03-21
*
Declaremods: a few syntactic improvements
letouzey
2013-03-13
*
Restrict (try...with...) to avoid catching critical exn (part 13)
letouzey
2013-03-13
*
Restrict (try...with...) to avoid catching critical exn (part 5)
letouzey
2013-03-13
*
kernel/declarations becomes a pure mli
letouzey
2013-02-26
*
Names: shortcuts for building {kn, constant, mind} with empty sections
letouzey
2013-02-26
*
Dir_path --> DirPath
letouzey
2013-02-19
*
Minor code cleanups, especially take advantage of Dir_path.is_empty
letouzey
2013-02-18
*
Uniformization of the "anomaly" command.
ppedrot
2013-01-28
*
Modulification of mod_bound_id
ppedrot
2012-12-18
*
Modulification of Label
ppedrot
2012-12-18
*
Modulification of dir_path
ppedrot
2012-12-14
*
Modulification of identifier
ppedrot
2012-12-14
*
Updating headers.
herbelin
2012-08-08
*
Fixing bug #2809 (anomaly when printing a module with notations due to
herbelin
2012-06-20
*
place all pretty-printing files in new dir printing/
letouzey
2012-05-29