coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
...
\| *	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
* \| \|	Removing constr generic argument.	Pierre-Marie Pédrot	2016-01-14
* \| \|	Removing ident and var generic arguments.	Pierre-Marie Pédrot	2016-01-14
* \| \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2016-01-13
\|\\| \|
\| * \|	Fixing #4467 (continued).	Hugo Herbelin	2016-01-13
\| * \|	Fixing #4467 (missing shadowing of variables in cases pattern).	Hugo Herbelin	2016-01-12
* \| \|	CLEANUP: removing unused field	Matej Kosik	2016-01-11
* \| \|	merge	Matej Kosik	2016-01-11
\|\ \ \
\| * \| \|	CLEANUP: kernel/context.ml{,i}	Matej Kosik	2016-01-11
* \| \| \|	Remove some unused functions.	Guillaume Melquiond	2016-01-02
* \| \| \|	Merge branch 'v8.5' into trunk	Guillaume Melquiond	2015-12-31
\|\ \ \ \ \| \| \|/ / \| \|/\| \|
* \| \| \|	Do not compose List.length with List.filter.	Guillaume Melquiond	2015-12-31
\| * \| \|	Do not dump a glob reference when its location is ghost. (Fix bug #4469)	Guillaume Melquiond	2015-12-31
* \| \| \|	Removing the special status of open_constr generic argument.	Pierre-Marie Pédrot	2015-12-28
* \| \| \|	Tentative API fix for tactic arguments to be fed to tclWITHHOLES.	Pierre-Marie Pédrot	2015-12-27
* \| \| \|	Do not compose "str" and "to_string" whenever possible.	Guillaume Melquiond	2015-12-22
* \| \| \|	Removing ad-hoc interpretation rules for tactic notations and their genarg.	Pierre-Marie Pédrot	2015-12-21
* \| \| \|	Sharing toplevel representation for several generic types.	Pierre-Marie Pédrot	2015-12-21
* \| \| \|	Changing the toplevel type of the int_or_var generic type to int.	Pierre-Marie Pédrot	2015-12-21
* \| \| \|	Removing the now useless genarg generic argument.	Pierre-Marie Pédrot	2015-12-21
\| \|/ / \|/\| \|
* \| \|	CLEANUP: the definition of the "Constrexpr.case_expr" type was simplified	Matej Kosik	2015-12-18
* \| \|	Getting rid of some hardwired generic arguments.	Pierre-Marie Pédrot	2015-12-17
\|/ /
* \|	Fix a bug in externalisation which prevented printing of projections	Matthieu Sozeau	2015-12-02
* \|	Make the pretty printer resilient to incomplete nametab (progress on #4363).	Enrico Tassi	2015-11-26
* \|	Fixing bug #3554: Anomaly: Anonymous implicit argument.	Pierre-Marie Pédrot	2015-11-11
* \|	Documenting a bit more interpretation functions in passing.	Hugo Herbelin	2015-10-26
* \|	Fix some typos.	Guillaume Melquiond	2015-10-13
* \|	Properly handle {\|...\|} patterns when patterns are not asymmetric. (Fix bug #...	Guillaume Melquiond	2015-09-16