coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
...
* \|	Safer API for constr_of_global, and getting rid of unsafe_constr_of_global.	Pierre-Marie Pédrot	2017-07-13
* \|	Less footguns in universe handling: remove subst_instance_context.	Pierre-Marie Pédrot	2017-07-11
* \|	Getting rid of simple calls to AUContext.instance.	Pierre-Marie Pédrot	2017-07-11
* \|	Bump year in headers.	Pierre-Marie Pédrot	2017-07-04
\| *	Remove dead code [Universes.simplify_universe_context]	Gaëtan Gilbert	2017-06-20
\|/
*	Clean up universes of constants and inductives	Amin Timany	2017-06-16
*	Squashed commit of the following:	Amin Timany	2017-06-16
*	Check subtyping of inductive types in Kernel	Amin Timany	2017-06-16
*	Using UInfoInd for universes in inductive types	Amin Timany	2017-06-16
*	New datastructure for universes of inductive types	Amin Timany	2017-06-16
*	Drop '.' from CErrors.anomaly, insert it in args	Jason Gross	2017-06-02
*	Remove unused [open] statements	Gaetan Gilbert	2017-04-27
*	Add [_] prefix to unused values which maybe should be kept	Gaetan Gilbert	2017-04-27
*	Merge branch 'trunk' into pr379	Maxime Dénès	2017-03-24
\|\
\| *	[pp] Remove uses of expensive string_of_ppcmds.	Emilio Jesus Gallego Arias	2017-03-21
* \|	Evarconv API using EConstr.	Pierre-Marie Pédrot	2017-02-14
\|/
*	Stronger static invariant in equality upto universes.	Pierre-Marie Pédrot	2016-10-31
*	Code factorization in Universes.	Pierre-Marie Pédrot	2016-10-31
*	Moving Universes to the engine/ folder.	Pierre-Marie Pédrot	2016-10-30