coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Generalize fix for auto from PMP to eauto and typeclasses eauto.	Matthieu Sozeau	2015-10-16
*	Exporting the original unprocessed hint in the hint running function.	Pierre-Marie Pédrot	2015-10-14
*	Fix bug #4354: interpret hints in the right env and sigma.	Matthieu Sozeau	2015-10-06
*	class_tactics: make interruptible	Enrico Tassi	2015-06-29
*	class_tactics: remove catch-all, use Errors.noncritical	Enrico Tassi	2015-06-29
*	Safer typing primitives.	Pierre-Marie Pédrot	2015-05-13
*	Rationalizing a bit the interface of Hints.	Pierre-Marie Pédrot	2015-05-11
*	Opaque implementation of auto tactics.	Pierre-Marie Pédrot	2015-04-14
*	Fix caching of local hintdb in typeclasses eauto.	Matthieu Sozeau	2015-04-09
*	Removing dead code.	Pierre-Marie Pédrot	2015-02-02
*	Revert "TCs: Properly handle Hint Extern with conclusions of the form _ -> _"	Matthieu Sozeau	2015-01-16
*	Add a (by default deactivated) option to force typeclass resolution to	Matthieu Sozeau	2015-01-15
*	Optionally allow eta-conversion during unification for type classes.	Matthieu Sozeau	2015-01-15
*	TCs: Properly handle Hint Extern with conclusions of the form _ -> _	Matthieu Sozeau	2015-01-13
*	Update headers.	Maxime Dénès	2015-01-12
*	Follow up to experimental eager evar unification in bcba6d1bc9:	Hugo Herbelin	2014-11-08
*	Remove the deprecated open-constr based refine.	Arnaud Spiwack	2014-10-22
*	Goal: remove some functions from the compatibility layer.	Arnaud Spiwack	2014-10-16
*	Fix for bug #3618.	Matthieu Sozeau	2014-10-15
*	Splitting out of auto.ml a file hints.ml dedicated to hints so as to	Hugo Herbelin	2014-10-07
*	Merging some functions from evarutil.ml/evd.ml.	Hugo Herbelin	2014-09-29
*	Be more conservative and keep the use of eq_constr in pretyping/ functions.	Matthieu Sozeau	2014-09-17
*	Fix bug #3593, making constr_eq and progress work up to	Matthieu Sozeau	2014-09-17
*	Add a "Hint Mode ref (+ \| -)*" hint for setting a global mode	Matthieu Sozeau	2014-09-15
*	Avoid backtracking in typeclass search if a solution for a closed	Matthieu Sozeau	2014-09-15
*	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
*	A step towards better differentiating when w_unify is used for subterm	Hugo Herbelin	2014-09-10
*	Renaming goal-entering functions.	Pierre-Marie Pédrot	2014-09-06
*	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