coq - The formal proof system

Age	Commit message (Expand)	Author
2018-01-22	[printing] Remove duplicate definitions of pr_lident and pr_lname	Vincent Laporte
2018-01-16	Merge PR #6499: [vernac] Move the flags/attributes out of vernac_expr	Maxime Dénès
2018-01-08	[vernac] vernac_expr no longer recursive	Vincent Laporte
2018-01-05	Brackets support single numbered goal selectors.	Théo Zimmermann
2017-12-23	[flags] Move global time flag into an attribute.	Emilio Jesus Gallego Arias
2017-12-20	Separate vernac controls and regular commands.	Maxime Dénès
2017-11-29	Remove "obsolete_locality" and fix STM vernac classification.	Maxime Dénès
2017-11-25	Allow local universe renaming in Print.	Gaëtan Gilbert
2017-11-21	[api] Miscellaneous consolidation + moves to engine.	Emilio Jesus Gallego Arias
2017-11-04	Finish removing Show Goal uid	Gaëtan Gilbert
2017-10-10	Parse [Proof using Type] without translating Type to an id.	Gaëtan Gilbert
2017-10-10	[vernac] Remove "Proof using" hacks from parser.	Emilio Jesus Gallego Arias
2017-10-03	Implementing a generic mechanism for locating named objects from Coq side.	Pierre-Marie Pédrot
2017-09-29	[vernac] Remove `Qed exporting` syntax.	Emilio Jesus Gallego Arias
2017-09-26	Merge PR #688: Binding universe constraints in Definition/Inductive/etc...	Maxime Dénès
2017-09-19	Remove STM vernaculars.	Maxime Dénès
2017-09-19	Allow declaring universe constraints at definition level.	Matthieu Sozeau
2017-09-15	Merge PR #939: [general] Merge parsing with highparsing, put toplevel at the ...	Maxime Dénès
2017-09-08	Parse directly to Sorts.family when appropriate.	Gaëtan Gilbert
2017-08-29	[vernac] Store Infix Modifier in Vernac Notation.	Pierre-Marie Pédrot
2017-07-31	Improve errors for cumulativity when monomorphic	Amin Timany
2017-07-19	Merge PR #770: [proof] Move bullets to their own module.	Maxime Dénès
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	Add printing of cumulativity in inductive types	Amin Timany
2017-06-16	Fix bugs and add an option for cumulativity	Amin Timany
2017-06-12	[proof] Move bullets to their own module.	Emilio Jesus Gallego Arias
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-02	Drop '.' from CErrors.anomaly, insert it in args	Jason Gross
2017-05-31	Creating a module Nameops.Name extending module Names.Name.	Hugo Herbelin
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-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	Remove some unused values and types	Gaetan Gilbert
2017-04-25	[location] [ast] Port module AST to CAst	Emilio Jesus Gallego Arias
2017-04-25	[location] [ast] Switch Constrexpr AST to an extensible node type.	Emilio Jesus Gallego Arias
2017-04-25	[location] Make location optional in Loc.located	Emilio Jesus Gallego Arias
2017-04-24	[location] Use Loc.located for constr_expr.	Emilio Jesus Gallego Arias
2017-04-24	[constrexpr] Make patterns use Loc.located for location information	Emilio Jesus Gallego Arias
2017-04-24	Merge PR#552: Miscelaneous commits	Maxime Dénès
2017-04-21	Remove VernacError	Gaetan Gilbert
2017-04-20	refactoring "Ppvernac.pr_extend"	Matej Kosik
2017-04-09	Removing internal support for accepting "{struct x}" and co in "Theorem with".	Hugo Herbelin
2017-03-24	[stm] Remove some obsolete vernacs/classification.	Emilio Jesus Gallego Arias
2017-03-21	[pp] Remove unused printing tagging infrastructure.	Emilio Jesus Gallego Arias
2016-12-07	Merge branch 'v8.6'	Pierre-Marie Pédrot
2016-12-02	Fixing printing of "Set Warnings Append".	Hugo Herbelin