coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	[option] Remove support for non-synchronous options.	Emilio Jesus Gallego Arias	2017-05-24
*	Merge branch 'trunk' into pr379	Maxime Dénès	2017-03-24
\|\
\| *	[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-03-21
* \|	Introducing contexts parameterized by the inner term type.	Pierre-Marie Pédrot	2017-02-14
\|/
*	Fix bug #4661: Cannot mask the absolute name.	Pierre-Marie Pédrot	2016-10-01
*	errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib mod...	Pierre Letouzey	2016-07-03
*	Removing dead code and unused opens.	Pierre-Marie Pédrot	2016-05-08
*	Merge branch 'v8.5'	Pierre-Marie Pédrot	2016-01-21
\|\
\| *	Update copyright headers.	Maxime Dénès	2016-01-20
* \|	merge	Matej Kosik	2016-01-11
\|\ \
\| * \|	CLEANUP: kernel/context.ml{,i}	Matej Kosik	2016-01-11
* \| \|	Do not compose "str" and "to_string" whenever possible.	Guillaume Melquiond	2015-12-22
\|/ /
* /	Moving extended_rel_vect/extended_rel_list to the kernel.	Hugo Herbelin	2015-12-05
\|/
*	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