coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Merge PR #6855: Update headers following #6543.	Maxime Dénès	2018-03-05
\|\
* \|	Handling evars in the VM.	Pierre-Marie Pédrot	2018-03-03
\| *	Update headers following #6543.	Théo Zimmermann	2018-02-27
\|/
*	Moving some universe substitution code out of the kernel.	Pierre-Marie Pédrot	2017-12-30
*	[lib] Rename Profile to CProfile	Emilio Jesus Gallego Arias	2017-12-09
*	[api] Deprecate all legacy uses of Names in core.	Emilio Jesus Gallego Arias	2017-11-06
*	Bump year in headers.	Pierre-Marie Pédrot	2017-07-04
*	use map_constr more efficiently	Amin Timany	2017-06-16
*	Use a smart map_constr	Amin Timany	2017-06-16
*	Drop '.' from CErrors.anomaly, insert it in args	Jason Gross	2017-06-02
*	More consistent writing of de Bruijn.	Théo Zimmermann	2017-05-01
*	Fixing injection in the presence of let-in in constructors.	Hugo Herbelin	2016-12-22
*	CLEANUP: minor readability improvements	Matej Kosik	2016-08-24
*	errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib mod...	Pierre Letouzey	2016-07-03
*	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
* \|	About building of substitutions from instances.	Hugo Herbelin	2015-12-05
* \|	Experimenting documentation of the Vars.subst functions.	Hugo Herbelin	2015-12-05
\|/
*	Adds support for the virtual machine to perform reduction of universe polymor...	Gregory Malecha	2015-10-28
*	Correct restriction of vm_compute when handling universe polymorphic	Matthieu Sozeau	2015-01-15
*	Update headers.	Maxime Dénès	2015-01-12
*	Move to a representation of universe polymorphic constants using indices for ...	Matthieu Sozeau	2014-08-03
*	Cleanup substitution inside universe instances, only done through subst_fn now,	Matthieu Sozeau	2014-07-21
*	- Fix hashing of levels to get the "right" order in universe contexts etc...	Matthieu Sozeau	2014-06-04
*	Various fixes of universe polymorphism and projections when they're set.	Matthieu Sozeau	2014-05-06
*	- Fix comparison of universes.	Matthieu Sozeau	2014-05-06
*	This commit adds full universe polymorphism and fast projections to Coq.	Matthieu Sozeau	2014-05-06
*	Remove some dead-code (thanks to ocaml warnings)	Pierre Letouzey	2014-03-05
*	Optimization in kernel/vars.ml: directly allocate a fixed-size block in the	Pierre-Marie Pédrot	2014-02-20
*	Less partial applications in Vars, as well as better memory allocation.	ppedrot	2013-11-06
*	Optimizing Vars.replace_vars	ppedrot	2013-10-23
*	Get rid of the uses of deprecated OCaml elements (still remaining compatible ...	xclerc	2013-09-19
*	Removing useless casts between arrays and lists.	ppedrot	2013-08-04
*	Splitting Term into five unrelated interfaces:	ppedrot	2013-04-29