coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Inductive.extract_stack,filter_stack_domain: remove unused arguments	Gaëtan Gilbert	2018-07-03
*	Remove Sorts.contents	Gaëtan Gilbert	2018-06-26
*	Using more general information for primitive records.	Pierre-Marie Pédrot	2018-06-23
*	Reduce circular dependency constants <-> projections	Gaëtan Gilbert	2018-05-31
*	Merge PR #407: Fix SR breakage due to allowing fixpoints on non-rec values	Maxime Dénès	2018-03-09
\|\
\| *	Fix SR breakage due to allowing fixpoints on non-rec values	Matthieu Sozeau	2018-03-08
* \|	Update headers following #6543.	Théo Zimmermann	2018-02-27
\|/
*	Fix #6621: Anomaly on fixpoint with primitive projections	Maxime Dénès	2018-01-24
*	[api] Also deprecate constructors of Decl_kinds.	Emilio Jesus Gallego Arias	2017-12-23
*	[lib] Rename Profile to CProfile	Emilio Jesus Gallego Arias	2017-12-09
*	Merge PR #486: Make some functions on terms more robust w.r.t new term constr...	Maxime Dénès	2017-11-24
\|\
\| *	Make some functions on terms more robust w.r.t new term constructs.	Maxime Dénès	2017-11-23
* \|	[api] Deprecate Term destructors, move to Constr	Emilio Jesus Gallego Arias	2017-11-22
\|/
*	[api] Move structures deprecated in the API to the core.	Emilio Jesus Gallego Arias	2017-11-06
*	kernel: bugfix in filter_stack_domain.	Matthieu Sozeau	2017-07-26
*	Less footguns in universe handling: remove subst_instance_context.	Pierre-Marie Pédrot	2017-07-11
*	Bump year in headers.	Pierre-Marie Pédrot	2017-07-04
*	Clean up universes of constants and inductives	Amin Timany	2017-06-16
*	Using UInfoInd for universes in inductive types	Amin Timany	2017-06-16
*	Drop '.' from CErrors.anomaly, insert it in args	Jason Gross	2017-06-02
*	[cleanup] Unify all calls to the error function.	Emilio Jesus Gallego Arias	2017-05-27
*	Introducing contexts parameterized by the inner term type.	Pierre-Marie Pédrot	2017-02-14
*	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
* \|	Moving the typing_flags to the environment.	Pierre-Marie Pédrot	2016-06-18
* \|	Merge PR #79: Let the kernel assume that a (co-)inductive type is positive.	Pierre-Marie Pédrot	2016-06-16
\|\ \
\| * \|	Assume totality: dedicated type rather than bool	Arnaud Spiwack	2016-06-14
* \| \|	Removing OCaml deprecated function names from the Lazy module.	Pierre-Marie Pédrot	2016-03-10
* \| \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2016-03-05
\|\ \ \ \| \| \|/ \| \|/\|
\| * \|	This fix is probably not enough to justify that there are no problems with	Maxime Dénès	2016-03-04
* \| \|	CLEANUP: Simplifying the changes done in "kernel/*"	Matej Kosik	2016-02-15
* \| \|	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
* \| \|	merge	Matej Kosik	2016-01-11
\|\ \ \
\| * \| \|	CLEANUP: kernel/context.ml{,i}	Matej Kosik	2016-01-11
* \| \| \|	Removing dead code.	Pierre-Marie Pédrot	2015-12-27
\|/ / /
* \| \|	Unifying betazeta_applist and prod_applist into a clearer interface.	Hugo Herbelin	2015-12-05
* \| \|	Moving extended_rel_vect/extended_rel_list to the kernel.	Hugo Herbelin	2015-12-05
* \| \|	Contracting one extra beta-redex on the fly when typing branches of "match".	Hugo Herbelin	2015-12-05
* \| \|	A few renaming and simplification in inductive.ml.	Hugo Herbelin	2015-12-05
\|/ /
* \|	Univs: be more restrictive for template polymorphic constants: only	Matthieu Sozeau	2015-10-12
* \|	Univs: fix bug #4251, handling of template polymorphic constants.	Matthieu Sozeau	2015-10-02
* \|	Univs/Inductive: fix typechecking of cases	Matthieu Sozeau	2015-07-15
* \|	Unused variables reported by OCaml.	Hugo Herbelin	2015-07-10
* \|	Kernel/Checker: Cleanup fixes of substitutions due to let-ins.	Matthieu Sozeau	2015-07-09
* \|	Template polymorphism: A bug-fix for Bug #4258	mlasson	2015-07-09
* \|	Univs: bug fix.	Matthieu Sozeau	2015-07-07