coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	instanciation is French, instantiation is English	Jason Gross	2014-08-25
*	Move UnsatisfiableConstraints to a pretype error.	Matthieu Sozeau	2014-08-22
*	Clenvtac.clenv_refine in the new monad. Not satisfactory though, because it	Pierre-Marie Pédrot	2014-06-24
*	Clenvtac.unify is in the new monad.	Pierre-Marie Pédrot	2014-06-23
*	Reindex section variables for typeclass resolution if their type changed.	Matthieu Sozeau	2014-06-21
*	Various fixes of universe polymorphism and projections when they're set.	Matthieu Sozeau	2014-05-06
*	This commit adds full universe polymorphism and fast projections to Coq.	Matthieu Sozeau	2014-05-06
*	Remove some dead-code (thanks to ocaml warnings)	Pierre Letouzey	2014-03-05
*	More Proofview.Goal.enter.	aspiwack	2013-11-02
*	A whole new implemenation of the refine tactic.	aspiwack	2013-11-02
*	A newly introduced variable inside a named context is no longer α-renamed.	aspiwack	2013-11-02
*	Clean-up: removed redundant notations (>>-) and (>>--) from Proofview.Notations.	aspiwack	2013-11-02
*	Getting rid of Goal.here, and all the related exceptions and combinators.	aspiwack	2013-11-02
*	Makes the new Proofview.tactic the basic type of Ltac.	aspiwack	2013-11-02
*	Removing uses of Evar.add in class-related functions.	ppedrot	2013-10-06
*	Moving side effects into evar_map. There was no reason to keep another	ppedrot	2013-10-05
*	Splitting Class_tactics between code and CAMLP4/5 declarations.	ppedrot	2013-10-04