coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	[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
*	Merge PR #841: Timorous fix of bug #5598 on global existing class in sections	Maxime Dénès	2017-08-16
\|\
* \|	Remove the function Global.type_of_global_unsafe.	Pierre-Marie Pédrot	2017-07-13
* \|	Getting rid of AUContext abstraction breakers in Discharge.	Pierre-Marie Pédrot	2017-07-13
* \|	Make the typeclass implementation fully compatible with universe polymorphism.	Pierre-Marie Pédrot	2017-07-13
* \|	Safer API for Global.type_of_global_in_context.	Pierre-Marie Pédrot	2017-07-13
* \|	Safe API for accessing universe constraints of global references.	Pierre-Marie Pédrot	2017-07-11
* \|	Bump year in headers.	Pierre-Marie Pédrot	2017-07-04
\| *	A fix for #5598 (no discharge of Existing Classes referring to local variables).	Hugo Herbelin	2017-06-28
\| *	Avoiding an optional int rather than using -1 to encode a local flag.	Hugo Herbelin	2017-06-28
\|/
*	Clean up universes of constants and inductives	Amin Timany	2017-06-16
*	Using UInfoInd for universes in inductive types	Amin Timany	2017-06-16
*	[cleanup] Unify all calls to the error function.	Emilio Jesus Gallego Arias	2017-05-27
*	[option] Remove support for non-synchronous options.	Emilio Jesus Gallego Arias	2017-05-24
*	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
* \|	Introducing contexts parameterized by the inner term type.	Pierre-Marie Pédrot	2017-02-14
* \|	Removing compatibility layers in Retyping	Pierre-Marie Pédrot	2017-02-14
* \|	Reductionops now return EConstrs.	Pierre-Marie Pédrot	2017-02-14
* \|	Eliminating parts of the right-hand side compatibility layer	Pierre-Marie Pédrot	2017-02-14
* \|	Typeclasses API using EConstr.	Pierre-Marie Pédrot	2017-02-14
* \|	Evarconv API using EConstr.	Pierre-Marie Pédrot	2017-02-14
* \|	Retyping API using EConstr.	Pierre-Marie Pédrot	2017-02-14
* \|	Reductionops API using EConstr.	Pierre-Marie Pédrot	2017-02-14
\| *	Merge branch 'v8.6'	Pierre-Marie Pédrot	2016-11-18
\|/\|
\| *	Lets Hints/Instances take an optional pattern	Matthieu Sozeau	2016-11-03
* \|	Merge branch 'v8.6'	Pierre-Marie Pédrot	2016-09-14
\|\\|
\| *	Fast path in Clenvtac.clenv_refine typeclass resolution.	Pierre-Marie Pédrot	2016-09-09
\| *	Monomorphize a costly boolean equality operation.	Pierre-Marie Pédrot	2016-09-09
* \|	CLEANUP: rename "Context.Named.{to,of}_rel" functions to "Context.Named.{to,o...	Matej Kosik	2016-08-26
* \|	CLEANUP: minor readability improvements	Matej Kosik	2016-08-24
* \|	Changing the definition of the "Lib.variable.info" type to enable us to do mo...	Matej Kosik	2016-08-24
\|/
*	errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib mod...	Pierre Letouzey	2016-07-03
*	Typeclasses:rename solve_instantiation* & use Hook	Matthieu Sozeau	2016-06-16
*	Removing dead code and unused opens.	Pierre-Marie Pédrot	2016-05-08
*	Pushing Proofview further down the dependency alley.	Pierre-Marie Pédrot	2016-03-20
*	merging conflicts with the original "trunk__CLEANUP__Context__2" branch	Matej Kosik	2016-02-15
\|\
* \	Merge branch 'v8.5'	Pierre-Marie Pédrot	2016-02-13
\|\ \
\| \| *	CLEANUP: Context.{Rel,Named}.Declaration.t	Matej Kosik	2016-02-09
\| \|/ \|/\|
\| *	More compact representation for evar resolvability flag.	Pierre-Marie Pédrot	2016-02-03
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2016-01-21
\|\\|
\| *	Update copyright headers.	Maxime Dénès	2016-01-20
* \|	merge	Matej Kosik	2016-01-11
\|\ \
\| * \|	CLEANUP: kernel/context.ml{,i}	Matej Kosik	2016-01-11
* \| \|	Do not compose List.length with List.filter.	Guillaume Melquiond	2015-12-31
\|/ /
* /	Moving extended_rel_vect/extended_rel_list to the kernel.	Hugo Herbelin	2015-12-05
\|/
*	Univs: fix many evar_map initializations and leaks.	Matthieu Sozeau	2015-10-02