coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Adding location to universes generated by the pretyper.	Pierre-Marie Pédrot	2016-02-19
*	merging conflicts with the original "trunk__CLEANUP__Context__2" branch	Matej Kosik	2016-02-15
\|\
* \|	Monotonizing the Evarutil module.	Pierre-Marie Pédrot	2016-02-15
\| *	CLEANUP: Context.{Rel,Named}.Declaration.t	Matej Kosik	2016-02-09
\|/
*	Merge branch 'v8.5'	Pierre-Marie Pédrot	2016-01-29
\|\
\| *	Fix bug #4519: oops, global shadowed local universe level bindings.	Matthieu Sozeau	2016-01-23
* \|	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
\|\\|
\| *	Fixing #4256 and #4484 (changes in evar-evar resolution made that new	Hugo Herbelin	2016-01-12
* \|	merge	Matej Kosik	2016-01-11
\|\ \
\| * \|	CLEANUP: kernel/context.ml{,i}	Matej Kosik	2016-01-11
* \| \|	Remove some unused functions.	Guillaume Melquiond	2016-01-02
* \| \|	Using dynamic values in tactic evaluation.	Pierre-Marie Pédrot	2015-12-21
\|/ /
* \|	Removing dynamic inclusion of constrs in tactic AST.	Pierre-Marie Pédrot	2015-12-04
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-11-29
\|\\|
\| *	Univs: entirely disallow instantiation of polymorphic constants with	Matthieu Sozeau	2015-11-27
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-11-15
\|\\|
\| *	Fix bug #4293: ensure let-ins do not contain algebraic universes in	Matthieu Sozeau	2015-11-11
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-11-05
\|\\|
\| *	Univs: update refman, better printers for universe contexts.	Matthieu Sozeau	2015-11-04
* \|	Merge branch 'v8.5' into trunk	Maxime Dénès	2015-10-16
\|\\|
\| *	Avoid dependency of the pretyper on C code.	Maxime Dénès	2015-10-15
\| *	Fix #4346 2/2: VM casts were not inferring universe constraints.	Maxime Dénès	2015-10-15
\| *	Fix #4346 1/2: native casts were not inferring universe constraints.	Maxime Dénès	2015-10-15
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-10-12
\|\\|
\| *	Refining 0c320e79ba30 in fixing interpretation of constr under binders	Hugo Herbelin	2015-10-11
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-10-09
\|\\|
\| *	Univs: fix bug #3807	Matthieu Sozeau	2015-10-08
\| *	Univs: add Strict Universe Declaration option (on by default)	Matthieu Sozeau	2015-10-07
* \|	Splitting kernel universe code in two modules.	Pierre-Marie Pédrot	2015-10-06
\|/
*	Univs (pretyping): call vm_compute/native_compute with the current	Matthieu Sozeau	2015-10-06
*	Univs: fix bug #4251, handling of template polymorphic constants.	Matthieu Sozeau	2015-10-02
*	Univs (pretyping): allow parsing and decl of Top.n	Matthieu Sozeau	2015-10-02
*	Continuing 817308ab (use ltac env for terms in ltac context) + fix	Hugo Herbelin	2015-08-02
*	Fixing #4221 (interpreting bound variables using ltac env was possibly	Hugo Herbelin	2015-08-02
*	Safer typing primitives.	Pierre-Marie Pédrot	2015-05-13
*	Fix some typos in comments.	Guillaume Melquiond	2015-02-23
*	Remove some dead code and add test-suite file.	Matthieu Sozeau	2015-02-16
*	Update headers.	Maxime Dénès	2015-01-12
*	When pretyping [uconstr] closures, don't use the local Ltac variable environm...	Arnaud Spiwack	2014-12-19
*	Getting rid of Exninfo hacks.	Pierre-Marie Pédrot	2014-12-16
*	Tentatively more informative report of failure when inferring	Hugo Herbelin	2014-12-11
*	uconstr: fix bug in interpretation of Ltac-bound name in let-tuple and patter...	Arnaud Spiwack	2014-11-19
*	Fixing bug #3792.	Pierre-Marie Pédrot	2014-11-09
*	Fixing confused code for interpretations of evar instances.	Hugo Herbelin	2014-11-03
*	Fixing inefficiency in typeclass resolution.	Pierre-Marie Pédrot	2014-11-03
*	This commit introduces changes in induction and destruct.	Hugo Herbelin	2014-10-25
*	Build unfolded versions of the primitive projection in let (a, p) := ...	Matthieu Sozeau	2014-10-07
*	Fixing interpretation of constr under binders which was broken after	Hugo Herbelin	2014-10-02