coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Make the typeclass implementation fully compatible with universe polymorphism.	Pierre-Marie Pédrot	2017-07-13
*	Bump year in headers.	Pierre-Marie Pédrot	2017-07-04
*	Using delayed universe instances in EConstr.	Pierre-Marie Pédrot	2017-04-01
*	Merge branch 'master'.	Pierre-Marie Pédrot	2017-02-14
\|\
* \|	Definining EConstr-based contexts.	Pierre-Marie Pédrot	2017-02-14
* \|	Class_tactics API using EConstr.	Pierre-Marie Pédrot	2017-02-14
* \|	Typeclasses API using EConstr.	Pierre-Marie Pédrot	2017-02-14
\| *	Lets Hints/Instances take an optional pattern	Matthieu Sozeau	2016-11-03
\|/
*	Fast path in Clenvtac.clenv_refine typeclass resolution.	Pierre-Marie Pédrot	2016-09-09
*	Typeclasses:rename solve_instantiation* & use Hook	Matthieu Sozeau	2016-06-16
*	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
\|/
*	Fix bug #3960: potential evar instance categorized as an unresolvable	Matthieu Sozeau	2015-02-16
*	Update headers.	Maxime Dénès	2015-01-12
*	Rework typeclass resolution and control of backtracking.	Matthieu Sozeau	2014-09-15
*	Add a flag for restricting resolution of typeclasses to	Matthieu Sozeau	2014-09-11
*	instanciation is French, instantiation is English	Jason Gross	2014-08-25
*	Add an option to solve typeclass goals generated by apply which can't be	Matthieu Sozeau	2014-07-31
*	- Fix treatment of global universe constraints which should be passed along	Matthieu Sozeau	2014-05-06
*	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