aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2020-11-06Intro pattern extensions for dup, swap and applyCyril Cohen
2020-11-06The "( X in t )" hack used in the syntax of ssr rewrite may be only parsing.Hugo Herbelin
2020-11-05Merge PR #12099: More parsing/printing notation/abbreviation consistency for ...Emilio Jesus Gallego Arias
2020-11-05Merge PR #12797: [refman] Take large chunks out of the tactics chapter.coqbot-app[bot]
2020-11-05Added change log for #12099.Hugo Herbelin
2020-11-05Minor cut elimination in the code of constrintern.ml.Hugo Herbelin
2020-11-05Regression tests for the various combinations of mixed terms and binders in n...Hugo Herbelin
2020-11-05Accept local variables in mixed terms and binders of notations.Hugo Herbelin
2020-11-05Accept section variables in notations with mixed terms and binders.Hugo Herbelin
2020-11-05Passing full interning env to pattern interning, for better control.Hugo Herbelin
2020-11-05Notations: Giving a consistent role to global references occurring patterns.Hugo Herbelin
2020-11-05Merge PR #13311: Changelog for 8.12.1.coqbot-app[bot]
2020-11-05Adding change log for #13217.Hugo Herbelin
2020-11-05Fixes #13216 (use of type classes in the return clause of a match).Hugo Herbelin
2020-11-05Fix macOS CI / disable bundle generation.Théo Zimmermann
2020-11-05Changelog for 8.12.1.Théo Zimmermann
2020-11-05Merge PR #12218: Numeral notations for non inductive typescoqbot-app[bot]
2020-11-05Merge PR #13301: Fixes #13298: Search applied to primitive projections needs ...coqbot-app[bot]
2020-11-05Add a redirection from previous location of the proof handling chapter.Théo Zimmermann
2020-11-05Improve title of first proof chapter.Théo Zimmermann
2020-11-05Change the title of the automatic tactic chapter and of its sections.Théo Zimmermann
2020-11-05Add new sections to automatic tactic chapter.Théo Zimmermann
2020-11-05Various fixes.Théo Zimmermann
2020-11-05Merge PR #13191: Fix anomaly when importing a functorPierre-Marie Pédrot
2020-11-05Merge content from two origins into the same file.Théo Zimmermann
2020-11-05Move proof handling chapter in new location.Théo Zimmermann
2020-11-05Octopus merge to preserve history of content split over multiple files.Théo Zimmermann
2020-11-05Remove everything before goal management.Théo Zimmermann
2020-11-05Remove everything after the content on goal management.Théo Zimmermann
2020-11-05Move some content on goal management to the proof mode page.Théo Zimmermann
2020-11-05Remove parts of Tactics that were moved elsewhere.Théo Zimmermann
2020-11-05Keep only the content on solvers for logic and equality.Théo Zimmermann
2020-11-05Move some content to a new page on solvers for logic and equality.Théo Zimmermann
2020-11-05Keep only content about auto.Théo Zimmermann
2020-11-05Move some content to a new page on automation.Théo Zimmermann
2020-11-05Add new page to writing proof index.Théo Zimmermann
2020-11-05Remove everything before term rewriting and simplification.Théo Zimmermann
2020-11-05Remove everything after term rewriting and simplification.Théo Zimmermann
2020-11-05Move some content to a new page on term rewriting and simplification.Théo Zimmermann
2020-11-05Merge PR #13231: Remove warning on SSR Search having moved.coqbot-app[bot]
2020-11-05Merge PR #13182: Check types when converting irrelevant terms in old unificationcoqbot-app[bot]
2020-11-04[stdlib] Decidable instance for negationYishuai Li
2020-11-05Add overlaysPierre Roux
2020-11-05Add changelogPierre Roux
2020-11-05Rename Dec and HexDec to Decimal and HexadecimalPierre Roux
2020-11-05[refman] Add an example for number notationsPierre Roux
2020-11-05Allow multiple primitive notation on the same scope and triggersPierre Roux
2020-11-05[string notation] Handle parameterized inductives and non inductivesPierre Roux
2020-11-05Merge numeral and string notation pluginsPierre Roux
2020-11-05[numeral notation] Add support for parameterized inductivesPierre Roux
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-04 07:56:11 +0000