coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Moving Eauto and Class_tactics to tactics/.	Pierre-Marie Pédrot	2016-03-25
*	Creating a dedicated ltac/ folder for Hightactics.	Pierre-Marie Pédrot	2016-03-21
*	merging conflicts with the original "trunk__CLEANUP__Context__2" branch	Matej Kosik	2016-02-15
\|\
* \|	Moving conversion functions to the new tactic API.	Pierre-Marie Pédrot	2016-02-15
\| *	CLEANUP: Context.{Rel,Named}.Declaration.t	Matej Kosik	2016-02-09
\|/
*	Merge branch 'v8.5'	Pierre-Marie Pédrot	2016-01-21
\|\
\| *	Update copyright headers.	Maxime Dénès	2016-01-20
* \|	Remove some unused functions.	Guillaume Melquiond	2016-01-02
* \|	Inlining the only use of Clenv.connect_clenv.	Pierre-Marie Pédrot	2015-11-18
* \|	Indexing Proofview.goals with a stage.	Pierre-Marie Pédrot	2015-10-20
* \|	Boxing the Goal.enter primitive into a record type.	Pierre-Marie Pédrot	2015-10-20
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-10-19
\|\\|
\| *	Generalize fix for auto from PMP to eauto and typeclasses eauto.	Matthieu Sozeau	2015-10-16
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-10-15
\|\\|
\| *	Exporting the original unprocessed hint in the hint running function.	Pierre-Marie Pédrot	2015-10-14
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-10-06
\|\\|
\| *	Fix bug #4354: interpret hints in the right env and sigma.	Matthieu Sozeau	2015-10-06
* \|	Add an Iterative Deepening search strategy to typeclass resolution.	Matthieu Sozeau	2015-07-27
* \|	Merge branch 'v8.5' into trunk	Maxime Dénès	2015-07-02
\|\\|
\| *	class_tactics: make interruptible	Enrico Tassi	2015-06-29
\| *	class_tactics: remove catch-all, use Errors.noncritical	Enrico Tassi	2015-06-29
* \|	Merge v8.5 into trunk	Hugo Herbelin	2015-05-15
\|\\|
\| *	Safer typing primitives.	Pierre-Marie Pédrot	2015-05-13
\| *	Rationalizing a bit the interface of Hints.	Pierre-Marie Pédrot	2015-05-11
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-04-15
\|\\|
\| *	Opaque implementation of auto tactics.	Pierre-Marie Pédrot	2015-04-14
* \|	Merge branch 'v8.5' into trunk	Pierre Letouzey	2015-04-09
\|\\|
\| *	Fix caching of local hintdb in typeclasses eauto.	Matthieu Sozeau	2015-04-09
* \|	Partially porting eauto to the new tactic API.	Pierre-Marie Pédrot	2015-02-23
\|/
*	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