coq - The formal proof system

Age	Commit message (Expand)	Author
2020-11-15	Doc and changelog for Instance Generalized Output	Gaëtan Gilbert
2020-11-14	Move destructuring let syntax closer to its documentation.	Théo Zimmermann
2020-11-12	Move last changelog entry for 8.12.1.	Théo Zimmermann
2020-11-12	Merge PR #13331: Fix #13330: Kernel messes with polymorphic side-effects.	coqbot-app[bot]
2020-11-12	Merge PR #13345: Addressing #13344: clarifying the role of Add ML Path vs -I	coqbot-app[bot]
2020-11-12	Add documentation about the soundness bug.	Pierre-Marie Pédrot
2020-11-12	Clarifying the role of Add ML Path vs -I (see #13344).	Hugo Herbelin
2020-11-12	Merge PR #13317: [ssr] intro pattern extensions for dup, swap and apply	coqbot-app[bot]
2020-11-10	Convert logic.rst to prodn	Jim Fehrle
2020-11-09	Add global version of OPTINREF	Jim Fehrle
2020-11-09	Merge PR #13329: [refman] Stop applying a special style to Coq, CoqIDE, OCaml...	coqbot-app[bot]
2020-11-09	[refman] Stop applying a special style to Coq, CoqIDE, OCaml and Gallina.	Théo Zimmermann
2020-11-09	Remove virtually unused replace rule.	Théo Zimmermann
2020-11-09	Fix #5226: Add index entry for ::=.	Théo Zimmermann
2020-11-09	Fix indentation of todo in Ltac chapter.	Théo Zimmermann
2020-11-06	Intro pattern extensions for dup, swap and apply	Cyril Cohen
2020-11-05	Merge PR #12797: [refman] Take large chunks out of the tactics chapter.	coqbot-app[bot]
2020-11-05	Changelog for 8.12.1.	Théo Zimmermann
2020-11-05	Merge PR #12218: Numeral notations for non inductive types	coqbot-app[bot]
2020-11-05	Add a redirection from previous location of the proof handling chapter.	Théo Zimmermann
2020-11-05	Improve title of first proof chapter.	Théo Zimmermann
2020-11-05	Change the title of the automatic tactic chapter and of its sections.	Théo Zimmermann
2020-11-05	Add new sections to automatic tactic chapter.	Théo Zimmermann
2020-11-05	Various fixes.	Théo Zimmermann
2020-11-05	Merge content from two origins into the same file.	Théo Zimmermann
2020-11-05	Move proof handling chapter in new location.	Théo Zimmermann
2020-11-05	Octopus merge to preserve history of content split over multiple files.	Théo Zimmermann
2020-11-05	Remove everything before goal management.	Théo Zimmermann
2020-11-05	Remove everything after the content on goal management.	Théo Zimmermann
2020-11-05	Move some content on goal management to the proof mode page.	Théo Zimmermann
2020-11-05	Remove parts of Tactics that were moved elsewhere.	Théo Zimmermann
2020-11-05	Keep only the content on solvers for logic and equality.	Théo Zimmermann
2020-11-05	Move some content to a new page on solvers for logic and equality.	Théo Zimmermann
2020-11-05	Keep only content about auto.	Théo Zimmermann
2020-11-05	Move some content to a new page on automation.	Théo Zimmermann
2020-11-05	Add new page to writing proof index.	Théo Zimmermann
2020-11-05	Remove everything before term rewriting and simplification.	Théo Zimmermann
2020-11-05	Remove everything after term rewriting and simplification.	Théo Zimmermann
2020-11-05	Move some content to a new page on term rewriting and simplification.	Théo Zimmermann
2020-11-05	Rename Dec and HexDec to Decimal and Hexadecimal	Pierre Roux
2020-11-05	[refman] Add an example for number notations	Pierre Roux
2020-11-05	[string notation] Handle parameterized inductives and non inductives	Pierre Roux
2020-11-05	[numeral notation] Add support for parameterized inductives	Pierre Roux
2020-11-05	[numeral notation] Handle implicit arguments	Pierre Roux
2020-11-05	[numeral notation] Document the via ... using ... option	Pierre Roux
2020-11-04	Regenerate the grammar description file.	Pierre-Marie Pédrot
2020-11-04	Document the syntax addition.	Pierre-Marie Pédrot
2020-11-03	Merge PR #13293: Doc: added "Arguments" removing implicit arguments	coqbot-app[bot]
2020-11-03	improved documentation of arguments command	Fabian Kunze
2020-11-02	Doc: added "Arguments" removing implicit arguments	Fabian Kunze