coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Fixing the checker w.r.t. wrongly used abstract universe contexts.	Pierre-Marie Pédrot	2017-07-19
*	Properly handling polymorphic inductive subtyping in the checker.	Pierre-Marie Pédrot	2017-07-11
*	Safe API for accessing universe constraints of global references.	Pierre-Marie Pédrot	2017-07-11
*	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
*	A short cleanup	Amin Timany	2017-06-16
*	use map_constr more efficiently	Amin Timany	2017-06-16
*	Optimization	Amin Timany	2017-06-16
*	Use a smart map_constr	Amin Timany	2017-06-16
*	Clean up universes of constants and inductives	Amin Timany	2017-06-16
*	Checker add test for non-trivial constraints	Amin Timany	2017-06-16
*	Properly instantiate contexts before pushing	Amin Timany	2017-06-16
*	Enable the checking of ind subtyping in checker	Amin Timany	2017-06-16
*	Correct coqchk checking subtyping relation for inductives	Amin Timany	2017-06-16
*	Correct coqchk reduction	Amin Timany	2017-06-16
*	Merge branch 'v8.6'	Pierre-Marie Pédrot	2017-06-08
\|\
* \|	Drop '.' from CErrors.anomaly, insert it in args	Jason Gross	2017-06-02
* \|	Merge PR#512: [cleanup] Unify all calls to the error function.	Maxime Dénès	2017-05-29
\|\ \
\| \| *	Fix a bug in checker	Amin Timany	2017-05-28
\| * \|	[cleanup] Unify all calls to the error function.	Emilio Jesus Gallego Arias	2017-05-27
* \| \|	[checker] [votour] resolve warning 52 fragile constant pattern	Gaëtan Gilbert	2017-05-26
* \| \|	[votour] Fix/disable warnings.	Emilio Jesus Gallego Arias	2017-05-26
* \| \|	[votour] Fix build with -safe-string (bug 5553)	Emilio Jesus Gallego Arias	2017-05-26
\|/ /
* \|	Merge branch 'trunk' into located_switch	Emilio Jesus Gallego Arias	2017-05-24
\|\ \
\| * \	Merge PR#411: Mention template polymorphism in the documentation.	Maxime Dénès	2017-05-03
\| \|\ \
\| * \ \	Merge PR#582: Fix warnings	Maxime Dénès	2017-05-02
\| \|\ \ \
\| * \| \| \|	More consistent writing of de Bruijn.	Théo Zimmermann	2017-05-01
\| \| * \| \|	Remove uses of [Flags.make_silent]	Gaetan Gilbert	2017-04-27
\| \| * \| \|	Remove some unused values and types	Gaetan Gilbert	2017-04-27
\| \| * \| \|	Remove unused [rec] keywords	Gaetan Gilbert	2017-04-27
\| \| * \| \|	Locally disable some warnings.	Gaetan Gilbert	2017-04-27
\| \|/ / /
* / / /	[location] Remove Loc.ghost.	Emilio Jesus Gallego Arias	2017-04-25
\|/ / /
\| * /	Update various comments to use "template polymorphism"	Gaetan Gilbert	2017-04-11
\|/ /
* \|	[pp] Remove uses of expensive string_of_ppcmds.	Emilio Jesus Gallego Arias	2017-03-21
* \|	Moving unused code out of the kernel into Termops.	Pierre-Marie Pédrot	2016-10-31
* \|	Merge branch 'v8.6'	Pierre-Marie Pédrot	2016-10-02
\|\\|
\| *	Merge remote-tracking branch 'github/pr/257' into v8.6	Maxime Dénès	2016-09-30
\| \|\
\| * \|	fix bug 3683 : adds references to the web site for the bug tracker	Yves Bertot	2016-09-29
* \| \|	Merge PR #244.	Pierre-Marie Pédrot	2016-09-08
\|\ \ \
\| * \| \|	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
\| * \| \|	Unify location handling of error functions.	Emilio Jesus Gallego Arias	2016-08-19
\|/ / /
\| \| *	[checker] Fix/fine tune printing.	Emilio Jesus Gallego Arias	2016-08-18
\| \|/
* /	remove checker/Makefile	Pierre Letouzey	2016-07-26
\|/
*	Merge remote-tracking branch 'gforge/v8.5' into v8.6	Matthieu Sozeau	2016-07-26
\|\
\| *	Fix bug #4876: critical bug in guard condition checker.	Matthieu Sozeau	2016-07-25
* \|	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