coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Fixing injection in the presence of let-in in constructors.	Hugo Herbelin	2016-12-22
*	Merge branch 'v8.5'	Pierre-Marie Pédrot	2016-01-21
\|\
\| *	Update copyright headers.	Maxime Dénès	2016-01-20
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2016-01-13
\|\\|
* \|	CLEANUP: kernel/context.ml{,i}	Matej Kosik	2016-01-11
\| *	Fix a misleading comment for substn_vars	Matthieu Sozeau	2016-01-07
* \|	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
*	This commit adds full universe polymorphism and fast projections to Coq.	Matthieu Sozeau	2014-05-06
*	Removing dead code, thanks to new OCaml warnings and a bit of scripting.	Pierre-Marie Pédrot	2014-04-23
*	A few fixes to the build system (mostly for ocamlbuild)	Pierre Letouzey	2013-12-16
*	comments in mli	pboutill	2013-05-30
*	Merging Context and Sign.	ppedrot	2013-04-29
*	Splitting Term into five unrelated interfaces:	ppedrot	2013-04-29