coq - The formal proof system

Age	Commit message (Expand)	Author
2019-06-01	Allowing Set to be part of universe expressions.	Hugo Herbelin
2019-06-01	Towards unifying parsing/printing for universe instances and Type's argument.	Hugo Herbelin
2019-05-23	do not parse `\|` as infix in patterns; parse `\|}` as `\|` `}`	Georges Gonthier
2019-05-16	binder_kind Generalized: remove 1st arg as it's always Implicit	Gaëtan Gilbert
2019-04-16	[ast] [constrexpr] Make recursion_order_expr an AST node.	Emilio Jesus Gallego Arias
2019-04-16	Clean the representation of recursive annotation in Constrexpr	Maxime Dénès
2019-04-02	Rename the INT token to NUMERAL	Pierre Roux
2019-04-01	Replace type sign = bool with SPlus \| SMinus	Pierre Roux
2019-03-14	Add a non-cumulative impredicative universe SProp.	Gaëtan Gilbert
2018-11-23	Remove the unsafe camlp5 API from the Coq codebase.	Pierre-Marie Pédrot
2018-10-05	Using smart mkLambdaCN/mkProdCN.	Hugo Herbelin
2018-09-02	Fixing #7867 (class error message tries to print a "fun" with no binder).	Hugo Herbelin
2018-07-29	Adding support for custom entries in notations.	Hugo Herbelin
2018-06-29	Port g_constr to the homebrew GEXTEND parser.	Pierre-Marie Pédrot