coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Merge branch 'trunk' into pr379	Maxime Dénès	2017-04-04
\|\
* \|	Using delayed universe instances in EConstr.	Pierre-Marie Pédrot	2017-04-01
\| *	Replacing "cast surgery" in LetIn by a proper field (see PR #404).	Hugo Herbelin	2017-03-24
\| *	Unifying standard "constr_level" names for constructors of local_binder_expr.	Hugo Herbelin	2017-03-24
* \|	Namegen primitives now apply on evar constrs.	Pierre-Marie Pédrot	2017-02-14
* \|	Definining EConstr-based contexts.	Pierre-Marie Pédrot	2017-02-14
* \|	Removing some return type compatibility layers in Termops.	Pierre-Marie Pédrot	2017-02-14
* \|	Tactics API using EConstr.	Pierre-Marie Pédrot	2017-02-14
* \|	Reductionops API using EConstr.	Pierre-Marie Pédrot	2017-02-14
* \|	Termops API using EConstr.	Pierre-Marie Pédrot	2017-02-14
\|/
*	CLEANUP: rename "Nameops.lift_subscript" to "Nameops.increment_subscript".	Matej Kosik	2016-10-19
*	Merge PR #244.	Pierre-Marie Pédrot	2016-09-08
\|\
* \|	CLEANUP: switching from "right-to-left" to "left-to-right" function compositi...	Matej Kosik	2016-08-30
* \|	CLEANUP: taking advantage of "_ % _" operator to express function composition...	Matej Kosik	2016-08-29
* \|	CLEANUP: minor readability improvements	Matej Kosik	2016-08-24
\| *	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
\|/
*	errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib mod...	Pierre Letouzey	2016-07-03
*	Reuse the typing_flags datatype for inductives.	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
\|\
* \|	Feedback cleanup	Emilio Jesus Gallego Arias	2016-05-31
* \|	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
* \| \|	CLEANUP: kernel/context.ml{,i}	Matej Kosik	2016-01-11
\|/ /
* \|	Univs: local names handling.	Matthieu Sozeau	2015-10-28
* \|	Fix some typos.	Guillaume Melquiond	2015-10-13
* \|	Univs: Add universe binding lists to definitions	Matthieu Sozeau	2015-09-14
\| *	Add corresponding field in `VernacInductive`.	Arnaud Spiwack	2015-06-24
\|/
*	Update headers.	Maxime Dénès	2015-01-12
*	kernel/ind Change interface of declare_mind and declare_mutual	Matthieu Sozeau	2015-01-05
*	Revert specific syntax for primitive projections, avoiding ugly	Matthieu Sozeau	2014-09-17
*	Uniformisation of the order of arguments env and sigma.	Hugo Herbelin	2014-09-12
*	Referring to evars by names. Added a parser for evars (but parsing of	Hugo Herbelin	2014-09-12
*	Print [Variant] types with the keyword [Variant].	Arnaud Spiwack	2014-09-04
*	Adapt Y. Bertot's path on private inductives (now the keyword is "Private").	Yves Bertot	2014-05-06
*	Initial work on reintroducing old-style polymorphism for compatibility (the s...	Matthieu Sozeau	2014-05-06
*	This commit adds full universe polymorphism and fast projections to Coq.	Matthieu Sozeau	2014-05-06
*	Removing the need of evarmaps in constr internalization.	Pierre-Marie Pédrot	2013-12-17
*	Removing a bunch of generic equalities.	ppedrot	2013-09-27
*	Splitting Term into five unrelated interfaces:	ppedrot	2013-04-29
*	Restrict (try...with...) to avoid catching critical exn (part 15)	letouzey	2013-03-13
*	Restrict (try...with...) to avoid catching critical exn (part 11)	letouzey	2013-03-13
*	use List.rev_map whenever possible	letouzey	2013-02-18
*	Modulification of name	ppedrot	2012-12-18
*	Modulification of identifier	ppedrot	2012-12-14
*	Monomorphized a lot of equalities over OCaml integers, thanks to	ppedrot	2012-11-08
*	Remove some more "open" and dead code thanks to OCaml4 warnings	letouzey	2012-10-02
*	More cleaning in CArray...	ppedrot	2012-09-18
*	As r15801: putting everything from Util.array_* to CArray.*.	ppedrot	2012-09-14