coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	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
*	Updating headers.	herbelin	2012-08-08
*	Separated notice vs info messages, and cleaned up the interface a bit.	ppedrot	2012-06-04
*	Cleaning Pp.ppnl use	ppedrot	2012-06-01
*	Getting rid of Pp.msgnl and Pp.message.	ppedrot	2012-06-01
*	global_reference migrated from Libnames to new Globnames, less deps in gramma...	letouzey	2012-05-29
*	Basic stuff about constr_expr migrated from topconstr to constrexpr_ops	letouzey	2012-05-29
*	New files intf/constrexpr.mli and intf/notation_term.mli out of Topconstr	letouzey	2012-05-29
*	Decl_kinds becomes a pure mli file, remaining ops in new file kindops.ml	letouzey	2012-05-29
*	Better error message when defining recursive records with Record or	aspiwack	2012-04-13
*	Second step of integration of Program:	msozeau	2012-03-14
*	Noise for nothing	pboutill	2012-03-02
*	Check for unresolved evars in textual order of the params and fields declarat...	msozeau	2012-01-25
*	Proof using ...	gareuselesinge	2011-12-12
*	Restore backward compatibility. ":>" declares subinstances in Class declarati...	msozeau	2011-11-18
*	Merge subinstances branch by me and Tom Prince.	msozeau	2011-11-17
*	Fixing bug #2181 (Class mechanism can create dependencies over unnamed	herbelin	2011-06-14
*	Revert "Add [Polymorphic] flag for defs"	msozeau	2011-04-13
*	Add [Polymorphic] flag for defs	msozeau	2011-04-13