coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Using more general information for primitive records.	Pierre-Marie Pédrot	2018-06-23
*	Change the proj_ind field from MutInd.t to inductive.	Pierre-Marie Pédrot	2018-06-23
*	Remove the proj_body field from the kernel.	Pierre-Marie Pédrot	2018-06-17
*	Getting rid of the const_proj field in the kernel.	Pierre-Marie Pédrot	2018-06-17
*	Reduce circular dependency constants <-> projections	Gaëtan Gilbert	2018-05-31
*	Split off Universes functions dealing with generating new universes.	Gaëtan Gilbert	2018-05-17
*	Merge PR #6926: An experimental 'Show Extraction' command (grant feature wish...	Maxime Dénès	2018-03-08
\|\
\| *	An experimental 'Show Extraction' command (grant feature wish #4129)	Pierre Letouzey	2018-03-06
\| *	Extraction: switch to EConstr.t as the central type to extract from.	Pierre Letouzey	2018-03-06
* \|	Update headers following #6543.	Théo Zimmermann	2018-02-27
\|/
*	[api] Also deprecate constructors of Decl_kinds.	Emilio Jesus Gallego Arias	2017-12-23
*	Make some functions on terms more robust w.r.t new term constructs.	Maxime Dénès	2017-11-23
*	[api] Move structures deprecated in the API to the core.	Emilio Jesus Gallego Arias	2017-11-06
*	Efficient fresh name generation relying on sets.	Pierre-Marie Pédrot	2017-09-28
*	Merge PR #909: Extraction: reduce primitive projections in types (fix bug 4709)	Maxime Dénès	2017-08-01
\|\
\| *	Extraction: reduce primitive projections in types (fix bug 4709)	Pierre Letouzey	2017-07-26
* \|	Removing template polymorphism for definitions.	Pierre-Marie Pédrot	2017-07-26
\|/
*	[API] Remove `open API` in ml files in favor of `-open API` flag.	Emilio Jesus Gallego Arias	2017-07-17
*	Bump year in headers.	Pierre-Marie Pédrot	2017-07-04
*	Remove (useless) aliases from the API.	Matej Košík	2017-06-10
*	Put all plugins behind an "API".	Matej Kosik	2017-06-07
*	Merge branch 'master'.	Pierre-Marie Pédrot	2017-02-14
\|\
* \|	Definining EConstr-based contexts.	Pierre-Marie Pédrot	2017-02-14
* \|	Removing compatibility layers in Retyping	Pierre-Marie Pédrot	2017-02-14
* \|	Reductionops now return EConstrs.	Pierre-Marie Pédrot	2017-02-14
* \|	Eliminating parts of the right-hand side compatibility layer	Pierre-Marie Pédrot	2017-02-14
* \|	Inv API using EConstr.	Pierre-Marie Pédrot	2017-02-14
* \|	Cleaning up opening of the EConstr module in pretyping folder.	Pierre-Marie Pédrot	2017-02-14
* \|	Unification API using EConstr.	Pierre-Marie Pédrot	2017-02-14
* \|	Retyping API using EConstr.	Pierre-Marie Pédrot	2017-02-14
* \|	Reductionops API using EConstr.	Pierre-Marie Pédrot	2017-02-14
* \|	Termops API using EConstr.	Pierre-Marie Pédrot	2017-02-14
\| *	Remove useless comments	Gaetan Gilbert	2017-01-28
\| *	Extend Fast_typeops to be a replacement for Typeops	Gaetan Gilbert	2016-12-12
\|/
*	Extraction: ignore some useless stuff about universes	Pierre Letouzey	2016-09-29
*	errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib mod...	Pierre Letouzey	2016-07-03
*	Separate flags for fix/cofix/match reduction and clean reduction function names.	Maxime Dénès	2016-07-01
*	Merge branch 'v8.5'	Pierre-Marie Pédrot	2016-06-27
\|\
\| *	Fix typo.	Guillaume Melquiond	2016-06-23
* \|	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