coq - The formal proof system

Age	Commit message (Expand)	Author
2017-09-19	Allow declaring universe binders with no constraints with @{\|}	Gaëtan Gilbert
2017-09-19	Allow declaring universe constraints at definition level.	Matthieu Sozeau
2017-09-19	Allow empty instance parsing @{}	Matthieu Sozeau
2017-09-15	Merge PR #939: [general] Merge parsing with highparsing, put toplevel at the ...	Maxime Dénès
2017-09-15	Merge PR #1051: Using an algebraic type for distinguishing toplevel input fro...	Maxime Dénès
2017-09-15	Merge PR #1037: Parse directly to Sorts.family when appropriate.	Maxime Dénès
2017-09-14	Using an algebraic type for distinguishing toplevel input from location in file.	Hugo Herbelin
2017-09-08	Parse directly to Sorts.family when appropriate.	Gaëtan Gilbert
2017-08-29	[general] Merge parsing with highparsing, put toplevel at the top of the link...	Emilio Jesus Gallego Arias
2017-08-29	[vernac] Store Infix Modifier in Vernac Notation.	Pierre-Marie Pédrot
2017-08-29	[parsing] Remove hacks for reduced Prelude.	Emilio Jesus Gallego Arias
2017-08-29	Merge PR #937: [general] Remove spurious dependency of highparsing on toplevel.	Maxime Dénès
2017-08-29	Merge PR #916: Fixing notation bug 5608 involving { } and a slight restructur...	Maxime Dénès
2017-08-29	Merge PR #773: [flags] Remove XML output flag.	Maxime Dénès
2017-08-29	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-16	Merge PR #864: Some cleanups after cumulativity for inductive types	Maxime Dénès
2017-08-01	[flags] Remove XML output flag.	Emilio Jesus Gallego Arias
2017-07-31	Improve errors for cumulativity when monomorphic	Amin Timany
2017-07-31	Change the option for cumulativity	Amin Timany
2017-07-31	[general] Remove spurious dependency of highparsing on toplevel.	Emilio Jesus Gallego Arias
2017-07-26	Adding support for recursive notations of the form "x , .. , y , z".	Hugo Herbelin
2017-07-04	Bump year in headers.	Pierre-Marie Pédrot
2017-06-21	[vernac] Remove stale bool parameter from `VernacStartTheoremProof`	Emilio Jesus Gallego Arias
2017-06-16	Change the option to Set Inductive Cumulativity	Amin Timany
2017-06-16	Fix bugs and add an option for cumulativity	Amin Timany
2017-06-15	Merge PR#719: Constrexpr.Numeral without bigint	Maxime Dénès
2017-06-14	Merge PR#765: Remove obsolete Show commands	Maxime Dénès
2017-06-14	Grammar hacks to get nice errors about non-loaded plugins (extr,recdef)	Pierre Letouzey
2017-06-14	G_prim: the bigint entry keeps numbers in raw strings	Pierre Letouzey
2017-06-14	Constrexpr.Numeral stays uninterpreted (string+sign instead of BigInt.t)	Pierre Letouzey
2017-06-12	Remove Show Thesis command which was never implemented.	Théo Zimmermann
2017-06-12	Remove non-working Show Tree and Show Node commands.	Théo Zimmermann
2017-06-12	Remove Show Implicit Arguments command.	Théo Zimmermann
2017-06-12	Remove Show Goal "uid" command.	Théo Zimmermann
2017-06-02	Drop '.' from CErrors.anomaly, insert it in args	Jason Gross
2017-05-27	[cleanup] Unify all calls to the error function.	Emilio Jesus Gallego Arias
2017-05-24	Merge branch 'trunk' into located_switch	Emilio Jesus Gallego Arias
2017-05-23	[vernac] Remove `Save thm id.` command.	Emilio Jesus Gallego Arias
2017-05-23	[vernac] Remove `Save.` command.	Emilio Jesus Gallego Arias
2017-05-16	Adding support for using grammar entries returning no value in EXTEND.	Hugo Herbelin
2017-05-03	Allow flexible anonymous universes in instances and sorts.	Gaetan Gilbert
2017-05-02	Merge PR#582: Fix warnings	Maxime Dénès
2017-04-28	Merge PR#531: Fixing bug #5420 and many similar bugs due to the presence of l...	Maxime Dénès
2017-04-27	Fix 4.04 warnings	Gaetan Gilbert
2017-04-27	Remove unused [open] statements	Gaetan Gilbert
2017-04-27	Remove unused constructors	Gaetan Gilbert
2017-04-27	Remove some unused values and types	Gaetan Gilbert
2017-04-27	Fix omitted labels in function calls	Gaetan Gilbert
2017-04-25	[location] [ast] Port module AST to CAst	Emilio Jesus Gallego Arias