coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Merge branch 'v8.5' into trunk	Maxime Dénès	2016-07-04
\|\
* \|	errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib mod...	Pierre Letouzey	2016-07-03
* \|	Fixing #4865 (deciding on which arguments to recompute scopes was not robust).	Hugo Herbelin	2016-06-29
* \|	A new infrastructure for warnings.	Maxime Dénès	2016-06-29
* \|	Properly handling the only printing flag when parsing rules already exist.	Pierre-Marie Pédrot	2016-06-28
\| *	Univs: allowing notations to take univ instances	Matthieu Sozeau	2016-06-27
\| *	Forbidding silently dropped universes instances in	Matthieu Sozeau	2016-06-27
* \|	Merge remote-tracking branch 'github/pr/223' into feedback-locations	Maxime Dénès	2016-06-27
\|\ \
* \| \|	minor: comment on the meaning of the 'boolean' variable	Gabriel Scherer	2016-06-27
* \| \|	minor: documentation comment for constrintern.ml:sort_fields	Gabriel Scherer	2016-06-27
* \| \|	minor: interp/constrintern.ml, clarify field completion	Gabriel Scherer	2016-06-27
* \| \|	minor: in constrintern.ml:sort_fields, clarify sf	Gabriel Scherer	2016-06-27
* \| \|	minor: in constrintern.ml:sort_fields, clarify build_patt	Gabriel Scherer	2016-06-27
* \| \|	whitespace: untabity constrinternl.ml:sort_fields	Gabriel Scherer	2016-06-27
* \| \|	minor clarifications in constrintern.ml:sort_fields	Gabriel Scherer	2016-06-27
* \| \|	Adding ability to put any pattern in binders, prefixed by a quote.	Daniel de Rauglaudre	2016-06-27
\| * \|	[feedback] Add optional ?loc parameter to loggers.	Emilio Jesus Gallego Arias	2016-06-25
\|/ /
* \|	Fixing #4854 (regression introduced in 4d25b224 in relation with #4592).	Hugo Herbelin	2016-06-24
* \|	Exporting a generic argument induction_arg. As a consequence,	Hugo Herbelin	2016-06-18
* \|	Being defensive in printing implicit arguments also with manual	Hugo Herbelin	2016-06-16
* \|	Not taking arguments given by name or position into account when	Hugo Herbelin	2016-06-16
* \|	Merge remote-tracking branch 'github/pr/194' into trunk	Maxime Dénès	2016-06-16
\|\ \
* \ \	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
\| \| *	Removing the use to Egramcoq.recover_constr_grammar.	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
\|\\|