coq - The formal proof system

Age	Commit message (Expand)	Author
2021-03-30	Remove the :> type cast	Jim Fehrle
2021-03-03	[build] Split stdlib to it's own opam package.	Emilio Jesus Gallego Arias
2021-01-13	Avoid using "subgoals" in the UI, it means the same as "goals"	Jim Fehrle
2020-12-21	Move evaluable_global_reference from Names to Tacred.	Pierre-Marie Pédrot
2020-11-25	Separate interning and pretyping of universes	Gaëtan Gilbert
2020-11-20	A step towards supporting pattern cast deeplier.	Hugo Herbelin
2020-11-20	Add preliminary support for notations with large class (non-recursive) binders.	Hugo Herbelin
2020-11-05	Merge PR #12218: Numeral notations for non inductive types	coqbot-app[bot]
2020-11-02	Nicer spacing when printing array literals	Gaëtan Gilbert
2020-11-02	Fix printing for empty primitive arrays	Gaëtan Gilbert
2020-10-30	Adding support for printing goal names in CoqIDE.	Hugo Herbelin
2020-10-30	Renaming Numeral into Number	Pierre Roux
2020-10-21	Rename the GlobRef comparison modules following the standard pattern.	Pierre-Marie Pédrot
2020-10-15	Merge PR #13140: Documenting Set Printing Goal Names + a small goal display fix	coqbot-app[bot]
2020-10-15	Merge PR #13144: Closes #13142: more standardized pretty-printing of Coq records	coqbot-app[bot]
2020-10-13	Merge PR #13099: Locating pattern identifiers (?id) by default at parsing tim...	Pierre-Marie Pédrot
2020-10-12	Merge PR #12874: Add a "Show Proof Diffs" message to the XML protocol	coqbot-app[bot]
2020-10-10	Add location in existential variable names (CEvar/GEvar).	Hugo Herbelin
2020-10-10	Adding and using locations on identifiers in constr_expr where they were miss...	Hugo Herbelin
2020-10-10	Closes #13142 (more standardized pretty-printing of records).	Hugo Herbelin
2020-10-09	Add an XML message for "Show Proof Diffs"	Jim Fehrle
2020-10-08	Dropping the misleading int argument of Pp.h.	Hugo Herbelin
2020-10-06	Fixing redundant outputs when printing goals, especially in non-"pr_first" mode.	Hugo Herbelin
2020-09-01	Unify the shelves	Maxime Dénès
2020-08-26	Move given_up goals to evar_map	Maxime Dénès
2020-07-15	Do not print global refs as terms when asked to be printed as themselves.	Hugo Herbelin
2020-07-06	Primitive persistent arrays	Maxime Dénès
2020-07-01	UIP in SProp	Gaëtan Gilbert
2020-07-01	Merge PR #12504: [states] Move States to vernac	Gaëtan Gilbert
2020-06-30	Merge PR #12599: Remove the Refiner module	Emilio Jesus Gallego Arias
2020-06-30	[states] Move States to vernac	Emilio Jesus Gallego Arias
2020-06-29	Moving the remaining Refiner functions to Tacmach.	Pierre-Marie Pédrot
2020-06-25	Generate names for anonymous polymorphic universes	Gaëtan Gilbert
2020-05-18	Improve spacing in Print Assumptions	Gaëtan Gilbert
2020-04-16	Make cumulative sprop a typing flag, deprecate command line -sprop-cumulative	Gaëtan Gilbert
2020-04-06	Clean and fix definitions of options.	Théo Zimmermann
2020-03-31	Merge PR #11647: [rfc] Consolidation of parsing interfaces	Pierre-Marie Pédrot
2020-03-30	Merge PR #11817: [cleanup] Remove unnecessary Map/Set module creation	Gaëtan Gilbert
2020-03-25	[parsing] Move `coq_parsable` custom logic to Grammar.	Emilio Jesus Gallego Arias
2020-03-22	Centralizing all kinds of numeral string management in numTok.ml.	Hugo Herbelin
2020-03-19	Merge PR #11795: Print implicit arguments in types of references	Hugo Herbelin
2020-03-18	Update headers in the whole code base.	Théo Zimmermann
2020-03-13	[cleanup] Remove unnecessary Map/Set module creation	Emilio Jesus Gallego Arias
2020-03-12	Print implicit arguments in types of references	SimonBoulier
2020-02-23	Cancelling precedences in Set Printing Parentheses only at border of notations.	Hugo Herbelin
2020-02-23	parens --> parentheses	Abhishek Anand (optiplex7010@home)
2020-02-23	bugfix: switched then/else: parens option false (default)=> no parens	Abhishek Anand (optiplex7010@home)
2020-02-23	added the new option	Abhishek Anand (optiplex7010@home)
2020-02-23	patched the print function	Abhishek Anand (optiplex7010@home)
2020-02-22	Simplification of type unparsing (index of variable in UnpMetaVar is unused).	Hugo Herbelin