coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	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-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
*	Fix bug #3960: potential evar instance categorized as an unresolvable	Matthieu Sozeau	2015-02-16
*	Removing dead code.	Pierre-Marie Pédrot	2015-02-02
*	Update headers.	Maxime Dénès	2015-01-12
*	Fixing new failure of #3017 after 012fe1a96ba81ab (Referring to evars	Hugo Herbelin	2014-10-01
*	For type classes, tell that VarInstance's behave like GoalEvar (avoid a loop ...	Hugo Herbelin	2014-09-18
*	Rework typeclass resolution and control of backtracking.	Matthieu Sozeau	2014-09-15
*	Referring to evars by names. Added a parser for evars (but parsing of	Hugo Herbelin	2014-09-12
*	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
*	Move to a representation of universe polymorphic constants using indices for ...	Matthieu Sozeau	2014-08-03
*	Existing Class now works with universe polymorphism. Fixes HoTT bug #063	Matthieu Sozeau	2014-06-17
*	- Fix treatment of global universe constraints which should be passed along	Matthieu Sozeau	2014-05-06
*	Adapt universe polymorphic branch to new handling of futures for delayed proofs.	Matthieu Sozeau	2014-05-06
*	Correct rebase on STM code. Thanks to E. Tassi for help on dealing with	Matthieu Sozeau	2014-05-06
*	This commit adds full universe polymorphism and fast projections to Coq.	Matthieu Sozeau	2014-05-06
*	At least made the evar type opaque! There are still 5 remaining unsafe	ppedrot	2013-09-18
*	Optimizing some evar_maps manipulation. In particular, using a [map] instead	ppedrot	2013-09-05
*	Actually using the domain function for maps.	ppedrot	2013-08-25
*	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
*	Delayed the computation of parameters in sort polymorphism of	herbelin	2013-05-14
*	Replacing compatibility layer for Fmap in Typeclasses. Code was	ppedrot	2013-05-14
*	More semantical-friendly function.	ppedrot	2013-05-14
*	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
*	code simplifications concerning Summary	letouzey	2013-04-22