coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Update headers following #6543.	Théo Zimmermann	2018-02-27
*	Adding general support for irrefutable disjunctive patterns.	Hugo Herbelin	2018-02-20
*	Adding support for parsing subterms of a notation as "pattern".	Hugo Herbelin	2018-02-20
*	Adding patterns in the category of binders for notations.	Hugo Herbelin	2018-02-20
*	More precise explanation when a notation is not reversible for printing.	Hugo Herbelin	2018-02-20
*	Making detyping potentially lazy.	Pierre-Marie Pédrot	2017-09-04
*	Bump year in headers.	Pierre-Marie Pédrot	2017-07-04
*	[location] Remove Loc.ghost.	Emilio Jesus Gallego Arias	2017-04-25
*	Using the same type of binders for interning and externing.	Hugo Herbelin	2017-03-24
*	Quick fix to #4595 (making notations containing "ltac:" unused for printing).	Hugo Herbelin	2016-10-04
*	Warning about similar notations now up to alpha-conversion.	Hugo Herbelin	2016-09-28
*	removing ocamldoc-related syntax errors	Matej Kosik	2016-07-12
*	Adding ability to put any pattern in binders, prefixed by a quote.	Daniel de Rauglaudre	2016-06-27
*	A slight phase of documentation and uniformization of names of	Hugo Herbelin	2016-06-02
*	Update copyright headers.	Maxime Dénès	2016-01-20
*	Fixing equality of notation_constrs. Fixes bug #4136.	Pierre-Marie Pédrot	2015-03-24
*	Update headers.	Maxime Dénès	2015-01-12
*	Remove many superfluous 'open' indicated by ocamlc -w +33	Pierre Letouzey	2014-03-05
*	Notations can now accept dummy arguments. If ever a bound variable is not	Pierre-Marie Pédrot	2013-12-22
*	Replacing uses of association lists by maps in notations.	ppedrot	2013-08-03
*	Modulification of name	ppedrot	2012-12-18
*	Modulification of identifier	ppedrot	2012-12-14
*	Added a constr_pattern_eq	ppedrot	2012-11-23
*	Updating headers.	herbelin	2012-08-08
*	Fixup implicits in patterns & notations	pboutill	2012-07-20
*	Added an indirection with respect to Loc in Compat. As many [open Compat]	ppedrot	2012-06-22
*	remove many excessive open Util & Errors in mli's	letouzey	2012-05-29
*	Stuff about notation_constr (ex-aconstr) now in notation_ops.ml	letouzey	2012-05-29