coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Merge branch 'v8.5'	Pierre-Marie Pédrot	2016-06-01
\|\
\| *	Extraction : add a location in the error message about polyprop	Pierre Letouzey	2016-05-30
* \|	Extraction : add a location in the error message about polyprop	Pierre Letouzey	2016-05-30
\| *	Extraction/Projections: Fix bug #4710	Matthieu Sozeau	2016-05-23
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2016-05-04
\|\\|
\| *	Handle primitive projections inside types when extracting (bug #4616).	Guillaume Melquiond	2016-05-04
* \|	CLEANUP: Context.{Rel,Named}.Declaration.t	Matej Kosik	2016-02-09
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2016-01-21
\|\\|
\| *	Update copyright headers.	Maxime Dénès	2016-01-20
* \|	CLEANUP: kernel/context.ml{,i}	Matej Kosik	2016-01-11
\|/
*	Extraction: more cautious use of intermediate result caching (fix #3923)	Pierre Letouzey	2015-12-15
*	Extraction: nicer implementation of Implicits	Pierre Letouzey	2015-12-12
*	Fix some typos.	Guillaume Melquiond	2015-12-07
*	Extraction: fix primitive projection extraction.	Matthieu Sozeau	2015-07-22
*	Update headers.	Maxime Dénès	2015-01-12
*	Extraction: no more ascii blob in type variables (fix #3227)	Pierre Letouzey	2015-01-11
*	Extraction : some more support functions for a future "Extraction Compute"	Pierre Letouzey	2015-01-11
*	Extraction: minor tweaks to ease ongoing experiments about Lambda	Pierre Letouzey	2015-01-11
*	library/opaqueTables: enable their use in interactive mode	Enrico Tassi	2014-10-13
*	Revert d0cd27e209be08ee51a2d609157367f053438a10: giving a different name	Matthieu Sozeau	2014-10-11
*	Add a boolean to indicate the unfolding state of a primitive projection,	Matthieu Sozeau	2014-09-27
*	Print [Variant] types with the keyword [Variant].	Arnaud Spiwack	2014-09-04
*	Change the way primitive projections are declared to the kernel.	Matthieu Sozeau	2014-08-28
*	instanciation is French, instantiation is English	Jason Gross	2014-08-25
*	A tentative uniform naming policy in module Inductiveops.	Hugo Herbelin	2014-08-01
*	Reuse universe level substitutions for template polymorphism, fixing performance	Matthieu Sozeau	2014-05-09
*	Fix extraction taking a type in the wrong environment.	Matthieu Sozeau	2014-05-06
*	Fix a pervasive equality use.	Matthieu Sozeau	2014-05-06
*	- Rename eq to equal in Univ, document new modules, set interfaces.	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
*	Fixing Pervasives.equality in extraction.	Pierre-Marie Pédrot	2014-03-03
*	Lazyconstr -> Opaqueproof	Enrico Tassi	2014-02-26
*	New compilation mode -vi2vo	Enrico Tassi	2014-02-26
*	More monomorphic List.mem + List.assoc + ...	letouzey	2013-10-24
*	Removing a bunch of generic equalities.	ppedrot	2013-09-27
*	Declarations.mli: reorganization of modular structures	letouzey	2013-08-20
*	State Transaction Machine	gareuselesinge	2013-08-08
*	Use the Hook module here and there.	ppedrot	2013-05-12
*	Splitting Term into five unrelated interfaces:	ppedrot	2013-04-29
*	Restrict (try...with...) to avoid catching critical exn (part 9)	letouzey	2013-03-13
*	Restrict (try...with...) to avoid catching critical exn (part 6)	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
*	Extraction: same as commit 16203, hopefully without NotASort exns	letouzey	2013-02-18
*	Fix extraction of inductive types that Coq auto-detects to be in Prop	letouzey	2013-02-14
*	Modulification of Label	ppedrot	2012-12-18
*	Extraction of projections: restrict a hack to ocaml only (fix #2941)	letouzey	2012-12-17
*	Modulification of identifier	ppedrot	2012-12-14
*	Moved Intset and Intmap to Int namespace.	ppedrot	2012-12-14