coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Update headers following #6543.	Théo Zimmermann	2018-02-27
*	Notations: Adding modifiers to tell which kind of binder a constr can parse.	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
*	Allows recursive patterns for binders to be associative on the left.	Hugo Herbelin	2018-02-20
*	A bit of miscellaneous code documentation around notations.	Hugo Herbelin	2018-02-20
*	More precise explanation when a notation is not reversible for printing.	Hugo Herbelin	2018-02-20
*	Use r.(p) syntax to print primitive projections.	Maxime Dénès	2018-01-30
*	[api] Move structures deprecated in the API to the core.	Emilio Jesus Gallego Arias	2017-11-06
*	A new step of restructuration of notations.	Hugo Herbelin	2017-08-29
*	A little reorganization of notations + a fix to #5608.	Hugo Herbelin	2017-08-29
*	Adding support for recursive notations of the form "x , .. , y , z".	Hugo Herbelin	2017-07-26
*	Bump year in headers.	Pierre-Marie Pédrot	2017-07-04
*	Put all plugins behind an "API".	Matej Kosik	2017-06-07