coq - The formal proof system

Age	Commit message (Expand)	Author
2020-11-09	Fix indentation of todo in Ltac chapter.	Théo Zimmermann
2020-11-09	[compat] remove 8.10	Enrico Tassi
2020-11-09	Merge PR #13217: Addresses #13216: use of type classes in the return clause o...	Pierre-Marie Pédrot
2020-11-06	Merge PR #13139: Clean the constr-as-hint API	coqbot-app[bot]
2020-11-06	Update doc/changelog/06-ssreflect/13317-ssr_dup_swap_apply_ipat.rst	Cyril Cohen
2020-11-06	Merge PR #13255: Fixes #13244: support for coercions in Search	coqbot-app[bot]
2020-11-06	Intro pattern extensions for dup, swap and apply	Cyril Cohen
2020-11-05	Merge PR #12099: More parsing/printing notation/abbreviation consistency for ...	Emilio Jesus Gallego Arias
2020-11-05	Merge PR #12797: [refman] Take large chunks out of the tactics chapter.	coqbot-app[bot]
2020-11-05	Added change log for #12099.	Hugo Herbelin
2020-11-05	Adding change log for #13217.	Hugo Herbelin
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	Merge PR #13301: Fixes #13298: Search applied to primitive projections needs ...	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-04	[stdlib] Decidable instance for negation	Yishuai Li
2020-11-05	Add changelog	Pierre Roux
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	Merge numeral and string notation plugins	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] Specify R	Pierre Roux
2020-11-05	[numeral notation] Document the via ... using ... option	Pierre Roux
2020-11-04	[numeral notation] Adding 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-04	Adding change log for #13255.	Hugo Herbelin
2020-11-04	Adding change log for #13301.	Hugo Herbelin
2020-11-04	Document the changes.	Pierre-Marie Pédrot