coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Merge branch 'v8.5'	Pierre-Marie Pédrot	2016-06-09
\|\
\| *	Fix bug #4777: Printing time is impacted by large terms that don't print.	Pierre-Marie Pédrot	2016-06-07
* \|	A slight phase of documentation and uniformization of names of	Hugo Herbelin	2016-06-02
* \|	Removing pointless field NPatVar. It does not make sense to have Meta	Hugo Herbelin	2016-06-02
* \|	Feedback cleanup	Emilio Jesus Gallego Arias	2016-05-31
* \|	Removing dead code and unused opens.	Pierre-Marie Pédrot	2016-05-08
* \|	Removing useless generic arguments.	Pierre-Marie Pédrot	2016-05-04
* \|	More toplevel value representation sharing.	Pierre-Marie Pédrot	2016-05-04
* \|	Moving the Val module to Geninterp.	Pierre-Marie Pédrot	2016-05-04
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2016-05-04
\|\\|
\| *	Increase the size of the dumpglob buffer for cooking notations (bug #4708).	Guillaume Melquiond	2016-05-04
\| *	Fix bug #3825: Universe annotations on notations should pass through or be re...	Pierre-Marie Pédrot	2016-05-03
* \|	Revert "A heuristic to add parentheses in the presence of rules such as"	Hugo Herbelin	2016-04-27
* \|	Revert "Not taking arguments given by name or position into account when"	Hugo Herbelin	2016-04-27
* \|	Revert "Being defensive in printing implicit arguments also with manual"	Hugo Herbelin	2016-04-27
* \|	Revert "Honor parsing and printing levels for tactic entry in TACTIC EXTEND and"	Hugo Herbelin	2016-04-27
* \|	Revert "Warn about possible shadowing of a name occurring in a "in" clause."	Hugo Herbelin	2016-04-27
* \|	Revert "Revert "Honor parsing and printing levels for tactic entry in TACTIC ...	Hugo Herbelin	2016-04-27
* \|	Revert "Honor parsing and printing levels for tactic entry in TACTIC EXTEND and"	Hugo Herbelin	2016-04-27
* \|	Warn about possible shadowing of a name occurring in a "in" clause.	Hugo Herbelin	2016-04-27
* \|	Honor parsing and printing levels for tactic entry in TACTIC EXTEND and	Hugo Herbelin	2016-04-27
* \|	Being defensive in printing implicit arguments also with manual	Hugo Herbelin	2016-04-27
* \|	Not taking arguments given by name or position into account when	Hugo Herbelin	2016-04-27
* \|	A heuristic to add parentheses in the presence of rules such as	Hugo Herbelin	2016-04-27
* \|	Fixing a "This clause is redundant" error when interpreting the "in"	Hugo Herbelin	2016-04-27
* \|	Reformatting + removal of some useless data + some cut-elimination	Hugo Herbelin	2016-04-27
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2016-04-24
\|\\|
\| *	Fixing #4677 (collision of a global variable and of a local variable	Hugo Herbelin	2016-04-19
* \|	Merge branch 'trunk-function_scope' of https://github.com/JasonGross/coq into...	Matthieu Sozeau	2016-04-04
\|\ \
* \| \|	Adding a new Ltac generic argument for forced tactics returing unit.	Pierre-Marie Pédrot	2016-03-20
* \| \|	Removing dead code in Genarg.	Pierre-Marie Pédrot	2016-03-19
* \| \|	Removing the special status of generic entries defined by Coq itself.	Pierre-Marie Pédrot	2016-03-17
* \| \|	Removing the registering of default values for generic arguments.	Pierre-Marie Pédrot	2016-03-17
* \| \|	Adopting the same rules for interpreting @, abbreviations and	Hugo Herbelin	2016-03-13
* \| \|	Supporting "(@foo) args" in patterns, where "@foo" has no arguments.	Hugo Herbelin	2016-03-13
* \| \|	A more explicit name to the asymmetric boolean flag.	Hugo Herbelin	2016-03-12
* \| \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2016-03-05
\|\ \ \ \| \| \|/ \| \|/\|
\| * \|	Fixing bug #4105: poor escaping in the protocol between CoqIDE and coqtop.	Pierre-Marie Pédrot	2016-03-03
* \| \|	Printing notations: Cleaning in anticipation of fixing #4592.	Hugo Herbelin	2016-02-28
* \| \|	The tactic generic argument now returns a value rather than a glob_expr.	Pierre-Marie Pédrot	2016-02-22
* \| \|	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
\|\ \ \ \ \| \| \|/ / \| \|/\| \|
\| * \| \|	Do not give a name to anonymous evars anymore. See bug #4547.	Pierre-Marie Pédrot	2016-02-13
\| \| * \|	CLEANUP: Context.{Rel,Named}.Declaration.t	Matej Kosik	2016-02-09
\| \|/ / \|/\| \|
* \| \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2016-01-29
\|\\| \|
\| * \|	Implement support for universe binder lists in Instance and Program Fixpoint/...	Matthieu Sozeau	2016-01-23
* \| \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2016-01-21
\|\\| \|
\| * \|	Update copyright headers.	Maxime Dénès	2016-01-20
* \| \|	Getting rid of the awkward unpack mechanism from Genarg.	Pierre-Marie Pédrot	2016-01-17
* \| \|	Temporary commit getting rid of Obj.magic unsafety for Genarg.	Pierre-Marie Pédrot	2016-01-17