coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	A slight phase of documentation and uniformization of names of	Hugo Herbelin	2016-06-02
*	Feedback cleanup	Emilio Jesus Gallego Arias	2016-05-31
*	Merge branch 'v8.5'	Pierre-Marie Pédrot	2016-05-04
\|\
\| *	Fix bug #3825: Universe annotations on notations should pass through or be re...	Pierre-Marie Pédrot	2016-05-03
* \|	Revert "Not taking arguments given by name or position into account when"	Hugo Herbelin	2016-04-27
* \|	Revert "Warn about possible shadowing of a name occurring in a "in" clause."	Hugo Herbelin	2016-04-27
* \|	Warn about possible shadowing of a name occurring in a "in" clause.	Hugo Herbelin	2016-04-27
* \|	Not taking arguments given by name or position into account when	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 'trunk-function_scope' of https://github.com/JasonGross/coq into...	Matthieu Sozeau	2016-04-04
\|\ \
* \| \|	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
* \| \|	Printing notations: Cleaning in anticipation of fixing #4592.	Hugo Herbelin	2016-02-28
* \| \|	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
* \| \|	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
* \| \| \|	Do not compose List.length with List.filter.	Guillaume Melquiond	2015-12-31
\|/ / /
* / /	CLEANUP: the definition of the "Constrexpr.case_expr" type was simplified	Matej Kosik	2015-12-18
\|/ /
* \|	Fixing bug #3554: Anomaly: Anonymous implicit argument.	Pierre-Marie Pédrot	2015-11-11
* \|	Properly handle {\|...\|} patterns when patterns are not asymmetric. (Fix bug #...	Guillaume Melquiond	2015-09-16
* \|	Fixing #4318 (anomaly when applying args to a recursive notation in patterns).	Hugo Herbelin	2015-08-21
\| *	Move type_scope into user space, fix some output logs	Jason Gross	2015-08-14
\|/
*	Fixing #4305 (compatibility wrt 8.4 in not interpreting an	Hugo Herbelin	2015-07-27
*	Fixing computation of implicit arguments by position in fixpoints (#4217).	Hugo Herbelin	2015-05-01
*	Fixing #3376 and #4191 (wrong index of maximally-inserted implicit argument	Hugo Herbelin	2015-04-21
*	Removing the unused field ltacrecvars of tactic internalization.	Pierre-Marie Pédrot	2015-02-27
*	Update headers.	Maxime Dénès	2015-01-12
*	Fixing #3892: Ensure that notation variables do not capture names	Hugo Herbelin	2014-12-30
*	Tentatively more informative report of failure when inferring	Hugo Herbelin	2014-12-11
*	Add syntax for naming new goals in refine: writing ?[id] instead of _	Hugo Herbelin	2014-09-30
*	Add a boolean to indicate the unfolding state of a primitive projection,	Matthieu Sozeau	2014-09-27
*	Revert specific syntax for primitive projections, avoiding ugly	Matthieu Sozeau	2014-09-17
*	Uniformisation of the order of arguments env and sigma.	Hugo Herbelin	2014-09-12
*	Parsing evar instances.	Hugo Herbelin	2014-09-12
*	Referring to evars by names. Added a parser for evars (but parsing of	Hugo Herbelin	2014-09-12
*	Parsing and printing of primitive projections, fix buggy behavior when	Matthieu Sozeau	2014-09-10
*	- Fix printing and parsing of primitive projections, including the Set	Matthieu Sozeau	2014-09-09
*	Parsing of Type@{max(i,j)}.	Matthieu Sozeau	2014-09-08
*	Change internalization of primitive projections to allow parsing [p t] as	Matthieu Sozeau	2014-08-08
*	Revert the change in Constrintern introduced by "Add a type of untyped term t...	Arnaud Spiwack	2014-08-06
*	Better fix of e5c025	Pierre Boutillier	2014-08-05
*	Fixing #3483 (graceful failing with notations to non-constructors in "match").	Hugo Herbelin	2014-08-03
*	Better struture for Ltac internalization environments in Constrintern.	Pierre-Marie Pédrot	2014-08-02
*	Faster uconstr.	Arnaud Spiwack	2014-08-01