coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Swapping Context and Constr: defining declarations on constr in Constr.	Hugo Herbelin	2018-06-27
*	[api] Misctypes removal: miscellaneous aliases.	Emilio Jesus Gallego Arias	2018-06-12
*	Move interning the [hint_pattern] outside the Typeclasses hooks.	Gaëtan Gilbert	2018-05-30
*	[api] Rename `global_reference` to `GlobRef.t` to follow kernel style.	Emilio Jesus Gallego Arias	2018-05-04
*	[api] Move `hint_info_expr` to `Typeclasses`.	Emilio Jesus Gallego Arias	2018-04-26
*	Merge PR #6855: Update headers following #6543.	Maxime Dénès	2018-03-05
\|\
* \|	comment "resolvability" bit in Evd.evar_map	Enrico Tassi	2018-02-27
\| *	Update headers following #6543.	Théo Zimmermann	2018-02-27
\|/
*	Remove the local polymorphic flag hack.	Maxime Dénès	2017-12-27
*	Merge PR #6289: Remove unused boolean from cl_context field of Typeclasses.ty...	Maxime Dénès	2017-12-27
\|\
* \|	[econstr] Cleanup in `vernac/classes.ml`.	Emilio Jesus Gallego Arias	2017-12-13
\| *	Remove unused boolean from cl_context field of Typeclasses.typeclass	Gaëtan Gilbert	2017-11-30
\|/
*	[api] Remove aliases of `Evar.t`	Emilio Jesus Gallego Arias	2017-11-26
*	[api] Move structures deprecated in the API to the core.	Emilio Jesus Gallego Arias	2017-11-06
*	[api] Deprecate all legacy uses of Names in core.	Emilio Jesus Gallego Arias	2017-11-06
*	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