coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Fixing bug #2951.	Pierre-Marie Pédrot	2015-03-08
*	Make native compiler handle universe polymorphic definitions.	Maxime Dénès	2015-01-17
*	Update headers.	Maxime Dénès	2015-01-12
*	kernel/ind Change interface of declare_mind and declare_mutual	Matthieu Sozeau	2015-01-05
*	Pass around information on the use of template polymorphism for	Matthieu Sozeau	2014-11-23
*	This commit introduces changes in induction and destruct.	Hugo Herbelin	2014-10-25
*	Revert d0cd27e209be08ee51a2d609157367f053438a10: giving a different name	Matthieu Sozeau	2014-10-11
*	Give the same argument name for the record binder of type class	Matthieu Sozeau	2014-10-10
*	Add syntax for naming new goals in refine: writing ?[id] instead of _	Hugo Herbelin	2014-09-30
*	Add a boolean to indicate the unfolding state of a primitive projection,	Matthieu Sozeau	2014-09-27
*	Rework typeclass resolution and control of backtracking.	Matthieu Sozeau	2014-09-15
*	Providing a -type-in-type option for collapsing the universe hierarchy.	Hugo Herbelin	2014-09-13
*	Uniformisation of the order of arguments env and sigma.	Hugo Herbelin	2014-09-12
*	Add a flag for restricting resolution of typeclasses to	Matthieu Sozeau	2014-09-11
*	Remove [Infer] option of records.	Arnaud Spiwack	2014-09-04
*	Types declared as Variants really do not accept recursive definitions.	Arnaud Spiwack	2014-09-04
*	Print [Variant] types with the keyword [Variant].	Arnaud Spiwack	2014-09-04
*	Simplify even further the declaration of primitive projections,	Matthieu Sozeau	2014-08-30
*	Fix bug when defining primitive projections mixing defined and abstracts fields.	Matthieu Sozeau	2014-08-29
*	Change the way primitive projections are declared to the kernel.	Matthieu Sozeau	2014-08-28
*	Move to a representation of universe polymorphic constants using indices for ...	Matthieu Sozeau	2014-08-03
*	- Do module substitution inside mind_record.	Matthieu Sozeau	2014-07-25
*	Cleanup treatment of template universe polymorphism (thanks to E. Tassi	Matthieu Sozeau	2014-06-20
*	Proofs now take and return an evar_universe_context, simplifying interfaces	Matthieu Sozeau	2014-06-18
*	Complying an ocaml warning.	Hugo Herbelin	2014-06-17
*	Safer entry point of primitive projections in the kernel, now it does recognize	Matthieu Sozeau	2014-06-17
*	Allow records whose sort is defined by a constant.	Matthieu Sozeau	2014-05-06
*	- Fix bug preventing apply from unfolding Fixpoints.	Matthieu Sozeau	2014-05-06
*	Adapt universe polymorphic branch to new handling of futures for delayed proofs.	Matthieu Sozeau	2014-05-06
*	Adapt Y. Bertot's path on private inductives (now the keyword is "Private").	Yves Bertot	2014-05-06
*	Rework handling of universes on top of the STM, allowing for delayed	Matthieu Sozeau	2014-05-06
*	This commit adds full universe polymorphism and fast projections to Coq.	Matthieu Sozeau	2014-05-06
*	Qed: feedback when type checking is done	Enrico Tassi	2013-12-24
*	Adding generic solvers to term holes. For now, no resolution mechanism nor	Pierre-Marie Pédrot	2013-11-27
*	cList: a few alternative to hashtbl-based uniquize, distinct, subset	letouzey	2013-10-23
*	Removing almost all new_untyped_evar, and a bunch of Evd.add.	ppedrot	2013-09-18
*	Unplugging Autoinstance. The code is still here if someone wishes	ppedrot	2013-09-12
*	State Transaction Machine	gareuselesinge	2013-08-08
*	A uniformization step around understand_* and interp_* functions.	herbelin	2013-05-09
*	Splitting Term into five unrelated interfaces:	ppedrot	2013-04-29
*	Added a Local Definition vernacular command. This type of definition	ppedrot	2013-03-11
*	Uniformization of the "anomaly" command.	ppedrot	2013-01-28
*	New implementation of the conversion test, using normalization by evaluation to	mdenes	2013-01-22
*	Modulification of name	ppedrot	2012-12-18
*	Modulification of identifier	ppedrot	2012-12-14
*	Monomorphization (toplevel)	ppedrot	2012-11-26
*	Taking into account the type of a definition (if it exists), and the	herbelin	2012-11-17
*	Remove some more "open" and dead code thanks to OCaml4 warnings	letouzey	2012-10-02
*	Moving Utils.list_* to a proper CList module, which includes stdlib	ppedrot	2012-09-14
*	This patch removes unused "open" (automatically generated from	regisgia	2012-09-14