coq - The formal proof system

Age	Commit message (Expand)	Author
2017-05-24	[option] Remove support for non-synchronous options.	Emilio Jesus Gallego Arias
2017-03-24	Merge branch 'trunk' into pr379	Maxime Dénès
2017-03-21	[pp] Move terminal-specific tagging to the toplevel.	Emilio Jesus Gallego Arias
2017-03-21	[pp] Prepare for serialization, remove opaque glue.	Emilio Jesus Gallego Arias
2017-03-21	[pp] Replace `Pp.Tag` by `Ppstyle.tag` = `string list`	Emilio Jesus Gallego Arias
2017-02-14	Introducing contexts parameterized by the inner term type.	Pierre-Marie Pédrot
2016-10-01	Fix bug #4661: Cannot mask the absolute name.	Pierre-Marie Pédrot
2016-07-03	errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib mod...	Pierre Letouzey
2016-05-08	Removing dead code and unused opens.	Pierre-Marie Pédrot
2016-01-21	Merge branch 'v8.5'	Pierre-Marie Pédrot
2016-01-20	Update copyright headers.	Maxime Dénès
2016-01-11	merge	Matej Kosik
2016-01-11	CLEANUP: kernel/context.ml{,i}	Matej Kosik
2015-12-22	Do not compose "str" and "to_string" whenever possible.	Guillaume Melquiond
2015-12-05	Moving extended_rel_vect/extended_rel_list to the kernel.	Hugo Herbelin
2015-10-28	Univs: local names handling.	Matthieu Sozeau
2015-10-28	Printing of @{} instances for polymorphic references in Print and About.	Matthieu Sozeau
2015-10-05	Univs: fix printing bug #3797.	Matthieu Sozeau
2015-07-27	Fixing bug #2169:	Pierre-Marie Pédrot
2015-01-12	Update headers.	Maxime Dénès
2015-01-11	Declarations.mli refactoring: module_type_body = module_body	Pierre Letouzey
2014-11-20	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-19	Adding rich-printing facilities to Printmod.	Pierre-Marie Pédrot
2014-09-12	Referring to evars by names. Added a parser for evars (but parsing of	Hugo Herbelin
2014-09-04	Print [Variant] types with the keyword [Variant].	Arnaud Spiwack
2014-08-25	"allows to", like "allowing to", is improper	Jason Gross
2014-05-06	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-03-05	Remove many superfluous 'open' indicated by ocamlc -w +33	Pierre Letouzey
2014-02-26	Lazyconstr -> Opaqueproof	Enrico Tassi
2013-10-24	Turn many List.assoc into List.assoc_f	letouzey
2013-08-20	Declarations.mli: reorganization of modular structures	letouzey
2013-07-17	Declaremods: major refactoring, stop duplicating libobjects in modules	letouzey
2013-03-21	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-13	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-02-26	kernel/declarations becomes a pure mli	letouzey
2013-02-26	Names: shortcuts for building {kn, constant, mind} with empty sections	letouzey
2013-02-19	Dir_path --> DirPath	letouzey
2013-02-18	Minor code cleanups, especially take advantage of Dir_path.is_empty	letouzey
2013-01-28	Uniformization of the "anomaly" command.	ppedrot
2012-12-18	Modulification of mod_bound_id	ppedrot
2012-12-18	Modulification of Label	ppedrot
2012-12-14	Modulification of dir_path	ppedrot
2012-12-14	Modulification of identifier	ppedrot
2012-08-08	Updating headers.	herbelin