coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	This commit adds full universe polymorphism and fast projections to Coq.	Matthieu Sozeau	2014-05-06
*	Remove many superfluous 'open' indicated by ocamlc -w +33	Pierre Letouzey	2014-03-05
*	Added printing of instance priority to the Print Instances command.	ppedrot	2013-08-01
*	One more fix for rewrite: disallow resolving of the (partial) constraints	msozeau	2013-06-12
*	Use the Hook module here and there.	ppedrot	2013-05-12
*	Merging Context and Sign.	ppedrot	2013-04-29
*	Splitting Term into five unrelated interfaces:	ppedrot	2013-04-29
*	Finer fix for bug 3017, mark unresolvability only of goals that are	msozeau	2013-04-18
*	Modulification of name	ppedrot	2012-12-18
*	Finish patch for Hint Resolve, stopping to generate new constant names for	msozeau	2012-12-08
*	Change Hint Resolve, Immediate to take a global reference as argument	msozeau	2012-10-26
*	Updating headers.	herbelin	2012-08-08
*	Forward-port fixes from 8.4 (15358, 15353, 15333).	msozeau	2012-06-04
*	remove many excessive open Util & Errors in mli's	letouzey	2012-05-29
*	global_reference migrated from Libnames to new Globnames, less deps in gramma...	letouzey	2012-05-29
*	Evar_kinds.mli containing former Evd.hole_kind, avoid deps on Evd	letouzey	2012-05-29
*	Fix interface of resolve_typeclasses: onlyargs -> with_goals:	msozeau	2012-03-20
*	Fix bugs related to Program integration.	msozeau	2012-03-19
*	Noise for nothing	pboutill	2012-03-02
*	Fix for Program Instance not separately checking the resolution of evars of t...	msozeau	2012-01-23
*	Restore backward compatibility. ":>" declares subinstances in Class declarati...	msozeau	2011-11-18
*	Merge subinstances branch by me and Tom Prince.	msozeau	2011-11-17
*	Fix bug #2557 and an issue with Propers for complement	msozeau	2011-10-07
*	- Make typeclass transparency information directly available	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
*	- Fix treatment of globality flag for typeclass instance hints (they	msozeau	2011-02-14
*	Misc improvements about evar_map	letouzey	2010-12-15
*	Fix bug #2321, allowing "_" named projections in classes. Not realizing	msozeau	2010-09-28
*	Updated all headers for 8.3 and trunk	herbelin	2010-07-24
*	New script dev/tools/change-header to automatically update Coq files headers.	herbelin	2010-06-22
*	Remove the svn-specific $Id$ annotations	letouzey	2010-04-29
*	Move from ocamlweb to ocamdoc to generate mli documentation	pboutill	2010-04-29
*	Here comes the commit, announced long ago, of the new tactic engine.	aspiwack	2010-04-22
*	Promote evar_defs to evar_map (in Evd)	glondu	2009-11-11
*	Integrate a few improvements on typeclasses and Program from the equations br...	msozeau	2009-10-28
*	Delete trailing whitespaces in all .{v,ml} files	glondu	2009-09-17
*	Fix the bug-ridden code used to choose leibniz or generalized	msozeau	2009-09-08
*	Use the proper unification flags in e_exact. This makes exact fail a bit	msozeau	2009-07-09
*	Fix exponential behaviour of the typeclasses persistent objects. Drop	puech	2008-12-06
*	Fix in the unification algorithm using evars: unify types of evar	msozeau	2008-11-05
*	Open notation for declaring record instances.	msozeau	2008-10-23
*	Fix bug #1943 and restrict the inference optimisation of Program to	msozeau	2008-09-15
*	Fix bug #1936: uncaught exception due to undefinable exceptions.	msozeau	2008-09-14
*	Fix bug #1940: uncaught exception when searching for a type class.	msozeau	2008-09-14
*	Fix bug in term dnet preventing some unifications. Allow "higher-order"	msozeau	2008-07-28
*	Even better test for choosing rewrite or setoid_rewrite.	msozeau	2008-07-26
*	Fixes in handling of implicit arguments:	msozeau	2008-07-04
*	Various bug fixes in type classes and subtac:	msozeau	2008-07-01
*	Code cleanup in typeclasses, remove dead and duplicated code.	msozeau	2008-06-21