coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Introduce a Pcoq.Entry module for functions that ought to be exported.	Pierre-Marie Pédrot	2018-07-07
*	Merge PR #7760: Fixes #7712 (an anomaly in reporting bad recursive notation f...	Emilio Jesus Gallego Arias	2018-07-01
\|\
* \|	Workaround to fix #7731 (printing not splitting line at break hint).	Hugo Herbelin	2018-06-29
\| *	Fixes #7712 (an anomaly in reporting bad recursive notation format).	Hugo Herbelin	2018-06-29
\|/
*	Remove reference name type.	Maxime Dénès	2018-06-18
*	[api] Misctypes removal: miscellaneous aliases.	Emilio Jesus Gallego Arias	2018-06-12
*	[notations] Split interpretation and parsing of notations	Emilio Jesus Gallego Arias	2018-05-31
*	[api] Make `vernac/` self-contained.	Emilio Jesus Gallego Arias	2018-05-27
*	Fixes #7462, part 2 (only-printing not make believe parsing rule is declared).	Hugo Herbelin	2018-05-10
*	[located] Push inner locations in `reference` to a CAst.t node.	Emilio Jesus Gallego Arias	2018-03-09
*	Update headers following #6543.	Théo Zimmermann	2018-02-27
*	[ast] Improve precision of Ast location recognition in serialization.	Emilio Jesus Gallego Arias	2018-02-22
*	Change default for notations with variables bound to both terms and binders.	Hugo Herbelin	2018-02-20
*	Notations: Adding modifiers to tell which kind of binder a constr can parse.	Hugo Herbelin	2018-02-20
*	Notations: A step in cleaning constr_entry_key.	Hugo Herbelin	2018-02-20
*	Moving Metasyntax.register_grammar to Pcoq for usability in Egramcoq.	Hugo Herbelin	2018-02-20
*	More flexibility in locating or referring to a notation.	Hugo Herbelin	2018-02-20
*	Being more flexible on format Adding a warning to be more informative	Hugo Herbelin	2018-02-20
*	Respecting the ident/pattern distinction in notation modifiers.	Hugo Herbelin	2018-02-20
*	Adding support for parsing subterms of a notation as "pattern".	Hugo Herbelin	2018-02-20
*	A bit of miscellaneous code documentation around notations.	Hugo Herbelin	2018-02-20
*	Introducing an intermediary type "constr_prod_entry_key" for grammar producti...	Hugo Herbelin	2018-02-20
*	Rephrasing ETBinderList with a self-documenting and invariant-carrying argument.	Hugo Herbelin	2018-02-20
*	More precise explanation when a notation is not reversible for printing.	Hugo Herbelin	2018-02-20
*	Change references to CAMLP4 to CAMLP5 to be more accurate since we no	Jim Fehrle	2018-02-17
*	Separate vernac controls and regular commands.	Maxime Dénès	2017-12-20
*	[api] Another large deprecation, `Nameops`	Emilio Jesus Gallego Arias	2017-11-13
*	Merge PR #1120: Fixing BZ#5762 (supporting implicit arguments in "where" clau...	Maxime Dénès	2017-10-20
\|\
* \	Merge PR #1062: BZ#5739, Allow level for leftmost nonterminal for printing-on...	Maxime Dénès	2017-10-09
\|\ \
\| \| *	Fixing #5762 (supporting imp. args. in "where" clause of an inductive def.).	Hugo Herbelin	2017-10-05
\| \|/ \|/\|
\| *	BZ#5739, Allow level for leftmost nonterminal for printing-ony Notations	Paul Steckler	2017-09-25
* \|	Merge PR #1057: Reporting locations in error messages about notation formats.	Maxime Dénès	2017-09-25
\|\ \
* \| \|	[flags] Flag `open Flags`	Emilio Jesus Gallego Arias	2017-09-20
\| \|/ \|/\|
\| *	Reporting locations in error messages about notation formats.	Hugo Herbelin	2017-09-18
\| *	Fixing two anomalies in corner cases of the syntax of notation formats.	Hugo Herbelin	2017-09-18
\|/
*	Fixing bug #5693 (treating empty notation format as any format).	Hugo Herbelin	2017-09-12
*	Quoting notations in incompatible-level error message.	Hugo Herbelin	2017-08-29
*	A new step of restructuration of notations.	Hugo Herbelin	2017-08-29
*	Dropping former fix to bug #5469 (notation format not recognizing curly braces).	Hugo Herbelin	2017-08-29
*	A little reorganization of notations + a fix to #5608.	Hugo Herbelin	2017-08-29
*	Merge PR #834: Adding support for recursive notations of the form "x , .. , y...	Maxime Dénès	2017-08-01
\|\
* \|	deprecate Pp.std_ppcmds type alias	Matej Košík	2017-07-27
\| *	Adding support for recursive notations of the form "x , .. , y , z".	Hugo Herbelin	2017-07-26
\|/
*	Merge branch 'v8.6'	Pierre-Marie Pédrot	2017-07-04
*	Bump year in headers.	Pierre-Marie Pédrot	2017-07-04
*	Merge branch 'v8.6'	Pierre-Marie Pédrot	2017-06-08
*	Drop '.' from CErrors.anomaly, insert it in args	Jason Gross	2017-06-02
*	[cleanup] Unify all calls to the error function.	Emilio Jesus Gallego Arias	2017-05-27
*	Merge branch 'trunk' into located_switch	Emilio Jesus Gallego Arias	2017-05-24
\|\
\| *	Remove some unused values and types	Gaetan Gilbert	2017-04-27