coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	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
*	- Add modulo_delta_types flag for unification to allow full	msozeau	2011-03-13
*	Keep information on which fields are subclasses in class declarations,	msozeau	2011-03-11
*	Interp a definition with the implicit arguments of its local context	pboutill	2011-02-10
*	Data structure telling implicits of local variables is a map in the	pboutill	2011-02-10
*	Remove the "Boxed" syntaxes and the const_entry_boxed field	letouzey	2011-01-28
*	More {raw => glob} changes for consistency	glondu	2010-12-24
*	Do not throw an error for anonymous generalized binders as they will be	msozeau	2010-11-18
*	Minor fixes from Gregory Malecha. A typo fixed and a better (located)	msozeau	2010-11-15
*	Added multiple implicit arguments rules per name.	herbelin	2010-10-03
*	Fix bug #2321, allowing "_" named projections in classes. Not realizing	msozeau	2010-09-28
*	Remove some occurrences of "open Termops"	glondu	2010-09-28
*	Fix function applications without labels (OCaml warning 6)	glondu	2010-09-28
*	Some dead code removal, thanks to Oug analyzer	letouzey	2010-09-24
*	* removed declare_constant and declare_internal_constant	vsiles	2010-09-02
*	v13392 port from v8.3 to trunk : correct message when defining inductive schemes	vsiles	2010-09-02
*	Updated all headers for 8.3 and trunk	herbelin	2010-07-24
*	Simplified the way internalization_data (i.e. bindings of bound vars	herbelin	2010-07-22