coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-02-26
\|\
\| *	Fixing bug #3298.	Pierre-Marie Pédrot	2015-02-26
\| *	Fixing printing of ordinals.	Pierre-Marie Pédrot	2015-02-26
\| *	[info_auto] & [info_trivial]: warning message to help users find [Info].	Arnaud Spiwack	2015-02-24
\| *	[info] tactical warning: do not suggest [info_auto] and [info_trivial].	Arnaud Spiwack	2015-02-24
* \|	Merge branch 'v8.5' into trunk	Enrico Tassi	2015-02-23
\|\\|
\| *	Fix some typos in comments.	Guillaume Melquiond	2015-02-23
* \|	Less compatibility layer in Eauto.	Pierre-Marie Pédrot	2015-02-23
* \|	Partially porting eauto to the new tactic API.	Pierre-Marie Pédrot	2015-02-23
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-02-23
\|\\|
\| *	Fixing error message when H already exists in tactic subexpression eqn:H.	Hugo Herbelin	2015-02-20
\| *	A fix for #3993 (not fully applied term to destruct when eqn is given).	Hugo Herbelin	2015-02-20
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-02-18
\|\\|
\| *	Fix bug #3938	Matthieu Sozeau	2015-02-18
\| *	Fixing bug #3944.	Pierre-Marie Pédrot	2015-02-16
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-02-15
\|\\|
\| *	Fixing bug #4016.	Pierre-Marie Pédrot	2015-02-14
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-02-13
\|\\|
\| *	Univs: fix bug #4031: wrong folding of sigma in change.	Matthieu Sozeau	2015-02-12
\| *	Fix bug #2775: Correct handling of universes in leminv.	Matthieu Sozeau	2015-02-12
\| *	Fixing compilation for 3.12.	Pierre-Marie Pédrot	2015-02-12
\| *	Tentative fix for bug #4027.	Pierre-Marie Pédrot	2015-02-12
\| *	Missing space in error message	Matěj Grabovský	2015-02-11
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-02-11
\|\\|
\| *	Fixing #4018 (uncaught exception on non-equality in intros [=]).	Hugo Herbelin	2015-02-10
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-02-10
\|\\|
\| *	More expressive API for tclWITHHOLES.	Pierre-Marie Pédrot	2015-02-10
\| *	Revert "Removing spurious tclWITHHOLES."	Pierre-Marie Pédrot	2015-02-10
\| *	Removing dead code.	Pierre-Marie Pédrot	2015-02-02
* \|	Merge branch 'v8.5' into trunk.	Pierre-Marie Pédrot	2015-01-25
\|\\|
\| *	Removed obsolete option "Legacy Partially Applied Elimination	Hugo Herbelin	2015-01-24
\| *	Tentative workaround for bug #3798.	Pierre-Marie Pédrot	2015-01-24
* \|	Splitting ML tactics in one function per grammar entry.	Pierre-Marie Pédrot	2015-01-23
* \|	Embedding the index of the ML tactic entry in the Tacexpr AST.	Pierre-Marie Pédrot	2015-01-21
* \|	Univs: proper printing of global and local universe names (only	Matthieu Sozeau	2015-01-18
* \|	Make native compiler handle universe polymorphic definitions.	Maxime Dénès	2015-01-18
* \|	Revert "TCs: Properly handle Hint Extern with conclusions of the form _ -> _"	Matthieu Sozeau	2015-01-18
* \|	Add a (by default deactivated) option to force typeclass resolution to	Matthieu Sozeau	2015-01-18
* \|	Optionally allow eta-conversion during unification for type classes.	Matthieu Sozeau	2015-01-18
\| *	Univs: proper printing of global and local universe names (only	Matthieu Sozeau	2015-01-17
\| *	Make native compiler handle universe polymorphic definitions.	Maxime Dénès	2015-01-17
\| *	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
*	Fixing compilation of penultimate commit d08532d.	Hugo Herbelin	2015-01-08
*	Avoiding introducing yet another convention in naming files.	Hugo Herbelin	2015-01-08
*	Fix setoid rewrite.	Arnaud Spiwack	2015-01-06
*	Fixing #3896 (incorrect sigma given to printer).	Hugo Herbelin	2015-01-03