coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	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
*	Fix my previous commit on ~polyprop	Pierre Letouzey	2015-05-12
*	Extraction: fix the detection of the "polyprop" situation	Pierre Letouzey	2015-05-12
*	Add support so that the type of a match in an inductive type with let-in	Hugo Herbelin	2015-02-27
*	Removing dead code.	Pierre-Marie Pédrot	2015-02-02
*	Make native compiler handle universe polymorphic definitions.	Maxime Dénès	2015-01-17
*	Update headers.	Maxime Dénès	2015-01-12
*	Fix some documentation typos.	Guillaume Melquiond	2015-01-06
*	Revert d0cd27e209be08ee51a2d609157367f053438a10: giving a different name	Matthieu Sozeau	2014-10-11
*	Fix generation of inductive elimination principle for primitive records.	Matthieu Sozeau	2014-09-10
*	Print [Variant] types with the keyword [Variant].	Arnaud Spiwack	2014-09-04
*	Change the way primitive projections are declared to the kernel.	Matthieu Sozeau	2014-08-28
*	Relax a bit the guard condition.	Maxime Dénès	2014-08-06
*	One more optimization for guard checking of cofixpoints.	Maxime Dénès	2014-08-04
*	More optimization in guard checking.	Maxime Dénès	2014-08-04
*	Fix an exponential behavior in guard checker for cofixpoints.	Maxime Dénès	2014-08-04
*	Move to a representation of universe polymorphic constants using indices for ...	Matthieu Sozeau	2014-08-03
*	A tentative uniform naming policy in module Inductiveops.	Hugo Herbelin	2014-08-01
*	Optimize check of new subterm relation on match.	Maxime Dénès	2014-07-31
*	Fix dynamic computation of recargs for mutual inductives.	Maxime Dénès	2014-07-31
*	Minor cleaning.	Maxime Dénès	2014-07-22
*	Revert "Extend subterm relation to pattern matching in return predicates."	Maxime Dénès	2014-07-22
*	Revert "Propagate size info through pattern matching in predicates, for the"	Maxime Dénès	2014-07-22
*	Propagate size info through pattern matching in predicates, for the	Maxime Dénès	2014-07-22
*	Extend subterm relation to pattern matching in return predicates.	Maxime Dénès	2014-07-22
*	Fix check_inductive_codomain.	Maxime Dénès	2014-07-22
*	Refine check_is_subterm.	Maxime Dénès	2014-07-22
*	Refined guard condition of cofixpoints, to anticipate potential futur	Maxime Dénès	2014-07-22
*	First attempt at a fix for guard condition on cofixpoints.	Maxime Dénès	2014-07-22
*	Typo in comment.	Maxime Dénès	2014-07-22