coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	[api] Deprecate Term destructors, move to Constr	Emilio Jesus Gallego Arias	2017-11-22
*	[api] Another large deprecation, `Nameops`	Emilio Jesus Gallego Arias	2017-11-13
*	[api] Move structures deprecated in the API to the core.	Emilio Jesus Gallego Arias	2017-11-06
*	[api] Deprecate all legacy uses of Names in core.	Emilio Jesus Gallego Arias	2017-11-06
*	unification: fix BZ#5692, recognize prim projs as CS projections	Matthieu Sozeau	2017-10-17
*	Properly handling projection parameters in canonical structures.	Pierre-Marie Pédrot	2017-10-17
*	Handling primitive projections in canonical structures.	Pierre-Marie Pédrot	2017-10-17
*	Getting rid of AUContext abstraction breakers in Recordops.	Pierre-Marie Pédrot	2017-07-13
*	Merge PR #870: Prepare De Bruijn universe abstractions, Episode I: Kernel	Maxime Dénès	2017-07-13
\|\
\| *	Safe API for accessing universe constraints of global references.	Pierre-Marie Pédrot	2017-07-11
* \|	Merge PR #863: Fixing environment in warning "Projection value has no head co...	Maxime Dénès	2017-07-07
\|\ \ \| \|/ \|/\|
\| *	Fixing environment in warning "Projection value has no head constant".	Hugo Herbelin	2017-07-07
* \|	Bump year in headers.	Pierre-Marie Pédrot	2017-07-04
\|/
*	Clean up universes of constants and inductives	Amin Timany	2017-06-16
*	Ltac now uses evar-based constrs.	Pierre-Marie Pédrot	2017-02-14
*	Reductionops now return EConstrs.	Pierre-Marie Pédrot	2017-02-14
*	Inv API using EConstr.	Pierre-Marie Pédrot	2017-02-14
*	Recordops 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
*	Make the user_err header an optional parameter.	Emilio Jesus Gallego Arias	2016-08-19
*	Remove errorlabstrm in favor of user_err	Emilio Jesus Gallego Arias	2016-08-19
*	Remove spurious warnings about projections when requiring modules.	Pierre-Marie Pédrot	2016-07-08
*	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
*	A new infrastructure for warnings.	Maxime Dénès	2016-06-29
*	Feedback cleanup	Emilio Jesus Gallego Arias	2016-05-31
*	Merge branch 'v8.5'	Pierre-Marie Pédrot	2016-01-21
\|\
\| *	Update copyright headers.	Maxime Dénès	2016-01-20
* \|	Do not compose List.length with List.filter.	Guillaume Melquiond	2015-12-31
\|/
*	Fix universe instantiation with canonical structures.	Maxime Dénès	2015-07-16
*	Update headers.	Maxime Dénès	2015-01-12
*	Documenting check_record + changing a possibly undefined int into int option.	Hugo Herbelin	2014-12-15
*	Switch the few remaining iso-latin-1 files to utf8	Pierre Letouzey	2014-12-09
*	Fix canonical structure resolution which was launched on the results of	Matthieu Sozeau	2014-09-26
*	Fast path in Canonical structure detection. We do not always compute the normal	Pierre-Marie Pédrot	2014-06-27
*	Removing dead code.	Pierre-Marie Pédrot	2014-06-17
*	- Fixes for canonical structure resolution (check that the initial term indee...	Matthieu Sozeau	2014-05-06
*	This commit adds full universe polymorphism and fast projections to Coq.	Matthieu Sozeau	2014-05-06
*	Fixing pervasive comparisons	Pierre-Marie Pédrot	2014-03-01
*	Stack operations of Reductionops in Reductionops.Stack	Pierre Boutillier	2014-02-24
*	Turn many List.assoc into List.assoc_f	letouzey	2013-10-24
*	Get rid of the uses of deprecated OCaml elements (still remaining compatible ...	xclerc	2013-09-19
*	Unplugging Autoinstance. The code is still here if someone wishes	ppedrot	2013-09-12
*	code simplifications concerning Summary	letouzey	2013-04-22
*	Restrict (try...with...) to avoid catching critical exn (part 12)	letouzey	2013-03-13
*	use List.rev_map whenever possible	letouzey	2013-02-18
*	Modulification of name	ppedrot	2012-12-18
*	Modulification of identifier	ppedrot	2012-12-14
*	Monomorphization (pretyping)	ppedrot	2012-11-22