From 6420bd11a8a0ce3b63d91de6825580c3efca049e Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Wed, 15 Jul 2026 12:53:52 +0200 Subject: [PATCH] changelog for 9.3+rc1 --- .mailmap | 3 + .../21416-record-postponed-eta-Changed.rst | 6 - ...21514-unfold-dep-heuristic-names-Added.rst | 11 - .../21531-stricter-type-in-type-Fixed.rst | 6 - .../21663-rr-match-global-sorts-Added.rst | 4 - .../21774-track-indices-matter-Added.rst | 6 - .../21845-guard-fix-subterm-Fixed.rst | 5 - .../21896-guard-incl-wf-paths-Fixed.rst | 5 - .../22058-einductive-contract-case-Fixed.rst | 5 - ...50-definitional_UIP_on_motives-Changed.rst | 6 - .../21450-elab-sorts-Added.rst | 4 - .../02-specification-language/21611-if-is.rst | 6 - .../21611-of-ampersand.rst | 7 - .../21627-intern-constr-in-tac-Fixed.rst | 6 - .../21899-janno-typeclasses-debug-Changed.rst | 5 - .../22123-deprecate-if-Deprecated.rst | 5 - .../22124-if-printing-Removed.rst | 4 - .../22170-belowtype-Fixed.rst | 6 - .../22207-record-with-Added.rst | 5 - .../21671-binder-constr-Changed.rst | 34 - .../03-notations/22194-master-Added.rst | 4 - .../04-tactics/20175-janno-unif-red-prim.rst | 6 - .../21521-strat-pattern-ltac-Added.rst | 5 - .../21631-stop-zeta-rewrite-Changed.rst | 5 - ...r-quotation-abstract-no-inline-Changed.rst | 7 - .../04-tactics/21811-genScheme-Changed.rst | 5 - .../21833-rm-non-global-hint-Removed.rst | 5 - .../21862-cleanup-hints-globref-Changed.rst | 9 - .../04-tactics/21928-arrayall-Changed.rst | 4 - .../21987-context-secvar-Changed.rst | 5 - .../04-tactics/21987-context-secvar-Fixed.rst | 11 - .../22001-gene-eqs-vars-Changed.rst | 6 - .../04-tactics/22154-fix-rec-Fixed.rst | 5 - .../04-tactics/22182-clear-shelf-Fixed.rst | 6 - .../04-tactics/22184-master-Changed.rst | 5 - .../22251-underp-proof-with-Changed.rst | 4 - .../21542-ltac2-scoped-notations-Added.rst | 7 - .../21558-ltac2-transparent-state-Added.rst | 6 - .../21617-tac2abbrev-up-Added.rst | 6 - .../21642-redoer-goals-Added.rst | 5 - .../21658-ltac2-scheme-lookup-Added.rst | 5 - .../21762-ltac2-strategy-Added.rst | 6 - .../21819-janno-ltac2-syntax-Added.rst | 4 - .../21881-sprop-case-scheme-Added.rst | 6 - .../22092-ltac2-match-level-Changed.rst | 4 - .../21478-ssreflect-rw-Changed.rst | 12 - .../21611-of-ampersand-of-Removed.rst | 5 - .../22096-fix-ssr-univpoly-Fixed.rst | 6 - .../07-ssreflect/22169-fix-22158-Fixed.rst | 5 - .../17266-alloc-limit-Added.rst | 4 - .../20660-search-fuzzy-Added.rst | 5 - .../21473-fix-printing-Fixed.rst | 5 - ...21578-fix-induction-scheme-sprop-Fixed.rst | 6 - .../21626-noverbose-Removed.rst | 7 - .../21645-print-regular-match-Added.rst | 4 - .../21779-set-indices-matter-Added.rst | 6 - .../21823-genAbout-Changed.rst | 4 - ...-print-assumptions-globals-types-Fixed.rst | 6 - .../21865-warn-missing-proof-Added.rst | 4 - .../21867-pr-debug-delta-resolver-Added.rst | 5 - .../21934-print-flat-Added.rst | 4 - ...ymmetric-patterns-no-implicits-Changed.rst | 8 - .../22017-GeneralizePrint-Changed.rst | 4 - .../22107-keep-using-Added.rst | 4 - .../22193-blacklist-search-table-Added.rst | 5 - .../22231-coqdep-warn-loc-Changed.rst | 5 - .../21423-rocq-wc-Proof-Fixed.rst | 5 - .../21950-coqdoc-alectryon-Added.rst | 4 - .../11-corelib/21971-number-nota-Changed.rst | 4 - .../22221-template-scheme-univs-Fixed.rst | 13 - .../21564-package-Added.rst | 13 - .../21660-recent-dune-Changed.rst | 4 - .../22198-relative-if-dune-Fixed.rst | 5 - ...21852-warnerror-legacy-loading-Removed.rst | 6 - doc/sphinx/changes.rst | 639 ++++++++++++++++++ doc/sphinx/language/extensions/match.rst | 2 + 76 files changed, 644 insertions(+), 445 deletions(-) delete mode 100644 doc/changelog/01-kernel/21416-record-postponed-eta-Changed.rst delete mode 100644 doc/changelog/01-kernel/21514-unfold-dep-heuristic-names-Added.rst delete mode 100644 doc/changelog/01-kernel/21531-stricter-type-in-type-Fixed.rst delete mode 100644 doc/changelog/01-kernel/21663-rr-match-global-sorts-Added.rst delete mode 100644 doc/changelog/01-kernel/21774-track-indices-matter-Added.rst delete mode 100644 doc/changelog/01-kernel/21845-guard-fix-subterm-Fixed.rst delete mode 100644 doc/changelog/01-kernel/21896-guard-incl-wf-paths-Fixed.rst delete mode 100644 doc/changelog/01-kernel/22058-einductive-contract-case-Fixed.rst delete mode 100644 doc/changelog/01-kernel/22150-definitional_UIP_on_motives-Changed.rst delete mode 100644 doc/changelog/02-specification-language/21450-elab-sorts-Added.rst delete mode 100644 doc/changelog/02-specification-language/21611-if-is.rst delete mode 100644 doc/changelog/02-specification-language/21611-of-ampersand.rst delete mode 100644 doc/changelog/02-specification-language/21627-intern-constr-in-tac-Fixed.rst delete mode 100644 doc/changelog/02-specification-language/21899-janno-typeclasses-debug-Changed.rst delete mode 100644 doc/changelog/02-specification-language/22123-deprecate-if-Deprecated.rst delete mode 100644 doc/changelog/02-specification-language/22124-if-printing-Removed.rst delete mode 100644 doc/changelog/02-specification-language/22170-belowtype-Fixed.rst delete mode 100644 doc/changelog/02-specification-language/22207-record-with-Added.rst delete mode 100644 doc/changelog/03-notations/21671-binder-constr-Changed.rst delete mode 100644 doc/changelog/03-notations/22194-master-Added.rst delete mode 100644 doc/changelog/04-tactics/20175-janno-unif-red-prim.rst delete mode 100644 doc/changelog/04-tactics/21521-strat-pattern-ltac-Added.rst delete mode 100644 doc/changelog/04-tactics/21631-stop-zeta-rewrite-Changed.rst delete mode 100644 doc/changelog/04-tactics/21676-constr-quotation-abstract-no-inline-Changed.rst delete mode 100644 doc/changelog/04-tactics/21811-genScheme-Changed.rst delete mode 100644 doc/changelog/04-tactics/21833-rm-non-global-hint-Removed.rst delete mode 100644 doc/changelog/04-tactics/21862-cleanup-hints-globref-Changed.rst delete mode 100644 doc/changelog/04-tactics/21928-arrayall-Changed.rst delete mode 100644 doc/changelog/04-tactics/21987-context-secvar-Changed.rst delete mode 100644 doc/changelog/04-tactics/21987-context-secvar-Fixed.rst delete mode 100644 doc/changelog/04-tactics/22001-gene-eqs-vars-Changed.rst delete mode 100644 doc/changelog/04-tactics/22154-fix-rec-Fixed.rst delete mode 100644 doc/changelog/04-tactics/22182-clear-shelf-Fixed.rst delete mode 100644 doc/changelog/04-tactics/22184-master-Changed.rst delete mode 100644 doc/changelog/04-tactics/22251-underp-proof-with-Changed.rst delete mode 100644 doc/changelog/06-Ltac2-language/21542-ltac2-scoped-notations-Added.rst delete mode 100644 doc/changelog/06-Ltac2-language/21558-ltac2-transparent-state-Added.rst delete mode 100644 doc/changelog/06-Ltac2-language/21617-tac2abbrev-up-Added.rst delete mode 100644 doc/changelog/06-Ltac2-language/21642-redoer-goals-Added.rst delete mode 100644 doc/changelog/06-Ltac2-language/21658-ltac2-scheme-lookup-Added.rst delete mode 100644 doc/changelog/06-Ltac2-language/21762-ltac2-strategy-Added.rst delete mode 100644 doc/changelog/06-Ltac2-language/21819-janno-ltac2-syntax-Added.rst delete mode 100644 doc/changelog/06-Ltac2-language/21881-sprop-case-scheme-Added.rst delete mode 100644 doc/changelog/06-Ltac2-language/22092-ltac2-match-level-Changed.rst delete mode 100644 doc/changelog/07-ssreflect/21478-ssreflect-rw-Changed.rst delete mode 100644 doc/changelog/07-ssreflect/21611-of-ampersand-of-Removed.rst delete mode 100644 doc/changelog/07-ssreflect/22096-fix-ssr-univpoly-Fixed.rst delete mode 100644 doc/changelog/07-ssreflect/22169-fix-22158-Fixed.rst delete mode 100644 doc/changelog/08-vernac-commands-and-options/17266-alloc-limit-Added.rst delete mode 100644 doc/changelog/08-vernac-commands-and-options/20660-search-fuzzy-Added.rst delete mode 100644 doc/changelog/08-vernac-commands-and-options/21473-fix-printing-Fixed.rst delete mode 100644 doc/changelog/08-vernac-commands-and-options/21578-fix-induction-scheme-sprop-Fixed.rst delete mode 100644 doc/changelog/08-vernac-commands-and-options/21626-noverbose-Removed.rst delete mode 100644 doc/changelog/08-vernac-commands-and-options/21645-print-regular-match-Added.rst delete mode 100644 doc/changelog/08-vernac-commands-and-options/21779-set-indices-matter-Added.rst delete mode 100644 doc/changelog/08-vernac-commands-and-options/21823-genAbout-Changed.rst delete mode 100644 doc/changelog/08-vernac-commands-and-options/21825-print-assumptions-globals-types-Fixed.rst delete mode 100644 doc/changelog/08-vernac-commands-and-options/21865-warn-missing-proof-Added.rst delete mode 100644 doc/changelog/08-vernac-commands-and-options/21867-pr-debug-delta-resolver-Added.rst delete mode 100644 doc/changelog/08-vernac-commands-and-options/21934-print-flat-Added.rst delete mode 100644 doc/changelog/08-vernac-commands-and-options/21947-asymmetric-patterns-no-implicits-Changed.rst delete mode 100644 doc/changelog/08-vernac-commands-and-options/22017-GeneralizePrint-Changed.rst delete mode 100644 doc/changelog/08-vernac-commands-and-options/22107-keep-using-Added.rst delete mode 100644 doc/changelog/08-vernac-commands-and-options/22193-blacklist-search-table-Added.rst delete mode 100644 doc/changelog/08-vernac-commands-and-options/22231-coqdep-warn-loc-Changed.rst delete mode 100644 doc/changelog/09-cli-tools/21423-rocq-wc-Proof-Fixed.rst delete mode 100644 doc/changelog/09-cli-tools/21950-coqdoc-alectryon-Added.rst delete mode 100644 doc/changelog/11-corelib/21971-number-nota-Changed.rst delete mode 100644 doc/changelog/11-corelib/22221-template-scheme-univs-Fixed.rst delete mode 100644 doc/changelog/12-infrastructure-and-dependencies/21564-package-Added.rst delete mode 100644 doc/changelog/12-infrastructure-and-dependencies/21660-recent-dune-Changed.rst delete mode 100644 doc/changelog/12-infrastructure-and-dependencies/22198-relative-if-dune-Fixed.rst delete mode 100644 doc/changelog/14-misc/21852-warnerror-legacy-loading-Removed.rst diff --git a/.mailmap b/.mailmap index f1565d1ba1b2..f5e87e56ba5a 100644 --- a/.mailmap +++ b/.mailmap @@ -37,6 +37,7 @@ Martin Bodin Martin Bodin Martin Bodin Mathis Bouverot MathisBD Ana Borges Ana +Peio Borthelle Lapin0t @drenched-moth < > drenched-moth <85354652+drenched-moth@users.noreply.github.com> Ana Borges ana-borges Felix Loyau-Kahn felixL-K @@ -47,6 +48,7 @@ Pierre Boutillier Pierre Pierre Boutillier Michele Caci mcaci Ali Caglayan Alizter +Matteo Calosci CalosciMatteo Arthur Charguéraud charguer chluebi <42419603+chluebi@users.noreply.github.com> chluebi <42419603+chluebi@users.noreply.github.com> Tej Chajed tchajed @@ -253,6 +255,7 @@ Enrico Tassi gares gares Romain Tetley rtetley Guillaume Munch-Maccagnoni gadmm +Dario Halilovic dhalilov Hendrik Tews Hendrik Tews Laurent Théry thery Laurent Théry thery diff --git a/doc/changelog/01-kernel/21416-record-postponed-eta-Changed.rst b/doc/changelog/01-kernel/21416-record-postponed-eta-Changed.rst deleted file mode 100644 index 6abac6d4c65b..000000000000 --- a/doc/changelog/01-kernel/21416-record-postponed-eta-Changed.rst +++ /dev/null @@ -1,6 +0,0 @@ -- **Changed:** - Sort-polymorphic records can now have primitive projections - with eta conversion depending on instantiation, - which is checked at runtime - (`#21416 `_, - by Tomas Diaz). diff --git a/doc/changelog/01-kernel/21514-unfold-dep-heuristic-names-Added.rst b/doc/changelog/01-kernel/21514-unfold-dep-heuristic-names-Added.rst deleted file mode 100644 index 8d077f0248c8..000000000000 --- a/doc/changelog/01-kernel/21514-unfold-dep-heuristic-names-Added.rst +++ /dev/null @@ -1,11 +0,0 @@ -- **Added:** - new flag :flag:`Kernel Conversion Dep Heuristic` that enables a heuristic for - smarter constant unfolding during conversion. When enabled, if two constants - have the same strategy level (see :cmd:`Strategy`) and one constant's - definition depends on the other, the dependent constant is unfolded first. - This can significantly speed up conversions in cases like checking ``c1 = - c2`` vs ``c2 = c1`` where one definition wraps the other. The flag defaults - to off, preserving the existing behavior of preferentially unfolding the - right-hand side first (`#21514 - `_, fixes `#21509 - `_, by Jason Gross). diff --git a/doc/changelog/01-kernel/21531-stricter-type-in-type-Fixed.rst b/doc/changelog/01-kernel/21531-stricter-type-in-type-Fixed.rst deleted file mode 100644 index 820ff4cb86e1..000000000000 --- a/doc/changelog/01-kernel/21531-stricter-type-in-type-Fixed.rst +++ /dev/null @@ -1,6 +0,0 @@ -- **Fixed:** - Unset Universe Checking doesn't confuse sorts anymore, only allowing Type in Type - (`#21531 `_, - fixes `#20241 `_ - and `#20667 `_, - by Yann Leray). diff --git a/doc/changelog/01-kernel/21663-rr-match-global-sorts-Added.rst b/doc/changelog/01-kernel/21663-rr-match-global-sorts-Added.rst deleted file mode 100644 index b7519df48ed5..000000000000 --- a/doc/changelog/01-kernel/21663-rr-match-global-sorts-Added.rst +++ /dev/null @@ -1,4 +0,0 @@ -- **Added:** - Added support for matching on specific global sorts in rewrite rules - (`#21663 `_, - by Yann Leray). diff --git a/doc/changelog/01-kernel/21774-track-indices-matter-Added.rst b/doc/changelog/01-kernel/21774-track-indices-matter-Added.rst deleted file mode 100644 index 4f298959c6cd..000000000000 --- a/doc/changelog/01-kernel/21774-track-indices-matter-Added.rst +++ /dev/null @@ -1,6 +0,0 @@ -- **Added:** - kernel now tracks reliance on ``-indices-matter`` not being passed, and - prints this information in the checker, and in :cmd:`Print Assumptions` - when ``-indices-matter`` is passed - (`#21774 `_, - by Jason Gross). diff --git a/doc/changelog/01-kernel/21845-guard-fix-subterm-Fixed.rst b/doc/changelog/01-kernel/21845-guard-fix-subterm-Fixed.rst deleted file mode 100644 index 0dda46ceba0e..000000000000 --- a/doc/changelog/01-kernel/21845-guard-fix-subterm-Fixed.rst +++ /dev/null @@ -1,5 +0,0 @@ -- **Fixed:** - Pass the correct environment in a reduction call inside the guard checker - (`#21845 `_, - fixes `#21839 `_, - by Yann Leray). diff --git a/doc/changelog/01-kernel/21896-guard-incl-wf-paths-Fixed.rst b/doc/changelog/01-kernel/21896-guard-incl-wf-paths-Fixed.rst deleted file mode 100644 index bd540c040004..000000000000 --- a/doc/changelog/01-kernel/21896-guard-incl-wf-paths-Fixed.rst +++ /dev/null @@ -1,5 +0,0 @@ -- **Fixed:** - Fix regression that prevented some mutual fixpoints involving nested inductives - (`#21896 `_, - fixes `#21892 `_, - by Yann Leray). diff --git a/doc/changelog/01-kernel/22058-einductive-contract-case-Fixed.rst b/doc/changelog/01-kernel/22058-einductive-contract-case-Fixed.rst deleted file mode 100644 index 1d99724dc98e..000000000000 --- a/doc/changelog/01-kernel/22058-einductive-contract-case-Fixed.rst +++ /dev/null @@ -1,5 +0,0 @@ -- **Fixed:** - ``EConstr.contract_case`` no longer anomalies when Case branches - contain evar-backed Lambda bodies (e.g., from ``Constr.in_context``) - (`#22058 `_, - by Jason Gross). diff --git a/doc/changelog/01-kernel/22150-definitional_UIP_on_motives-Changed.rst b/doc/changelog/01-kernel/22150-definitional_UIP_on_motives-Changed.rst deleted file mode 100644 index cc4b6e2f7d94..000000000000 --- a/doc/changelog/01-kernel/22150-definitional_UIP_on_motives-Changed.rst +++ /dev/null @@ -1,6 +0,0 @@ -- **Changed:** - Check convertibility of the motive applied to indices instead of directly convertibility of indices - (when `Set Definitional UIP` is enabled). - This is a stronger reduction rule that subsumes the previous one and is justified by a proof using logical relations - (`#22150 `_, - by nicolas tabareau). diff --git a/doc/changelog/02-specification-language/21450-elab-sorts-Added.rst b/doc/changelog/02-specification-language/21450-elab-sorts-Added.rst deleted file mode 100644 index a09b4fd15bb6..000000000000 --- a/doc/changelog/02-specification-language/21450-elab-sorts-Added.rst +++ /dev/null @@ -1,4 +0,0 @@ -- **Added:** - elaboration of implicit sort qualities, controlled by the flag :flag:`Collapse Sorts ToType` - (`#21450 `_, - by Tomas Diaz). diff --git a/doc/changelog/02-specification-language/21611-if-is.rst b/doc/changelog/02-specification-language/21611-if-is.rst deleted file mode 100644 index 9e3a1ff02396..000000000000 --- a/doc/changelog/02-specification-language/21611-if-is.rst +++ /dev/null @@ -1,6 +0,0 @@ -- **Added:** - new syntactic sugar `if g is c then t else e` - for `match g with c => t | _ => e end`. This adds the - new reserved keyword `is` - (`#21478 `_, - by Pierre Roux). diff --git a/doc/changelog/02-specification-language/21611-of-ampersand.rst b/doc/changelog/02-specification-language/21611-of-ampersand.rst deleted file mode 100644 index 0f086e21b45d..000000000000 --- a/doc/changelog/02-specification-language/21611-of-ampersand.rst +++ /dev/null @@ -1,7 +0,0 @@ -- **Added:** - new syntactic sugars `& T` for anonymous binders `(_ : T)` - and `of T & ... & T` for anonymous binders in constructors, enabling the - `Variant t := C1 of a & b & c | C2 x y of P x & Q y.` syntax. - This adds the new reserved keyword `of` - (`#21611 `_, - by Pierre Roux). diff --git a/doc/changelog/02-specification-language/21627-intern-constr-in-tac-Fixed.rst b/doc/changelog/02-specification-language/21627-intern-constr-in-tac-Fixed.rst deleted file mode 100644 index ed227ace742b..000000000000 --- a/doc/changelog/02-specification-language/21627-intern-constr-in-tac-Fixed.rst +++ /dev/null @@ -1,6 +0,0 @@ -- **Fixed:** - tactic definitions (:cmd:`Ltac`, :cmd:`Ltac2`, tactic notations, etc) - correctly check that universe names are declared instead of delaying the error to when the tactic is used - (`#21627 `_, - fixes `#21616 `_, - by Gaëtan Gilbert). diff --git a/doc/changelog/02-specification-language/21899-janno-typeclasses-debug-Changed.rst b/doc/changelog/02-specification-language/21899-janno-typeclasses-debug-Changed.rst deleted file mode 100644 index 45ef9e57768c..000000000000 --- a/doc/changelog/02-specification-language/21899-janno-typeclasses-debug-Changed.rst +++ /dev/null @@ -1,5 +0,0 @@ -- **Changed:** - External hints now emit a new log entry starting with "running HINT on GOAL" before the tactic code is executed; all hints had their log entry for a successful application changed from just "HINT on GOAL" to "applied HINT on GOAL" - (`#21899 `_, - fixes `#21898 `_, - by Jan-Oliver Kaiser). diff --git a/doc/changelog/02-specification-language/22123-deprecate-if-Deprecated.rst b/doc/changelog/02-specification-language/22123-deprecate-if-Deprecated.rst deleted file mode 100644 index 2c0850820676..000000000000 --- a/doc/changelog/02-specification-language/22123-deprecate-if-Deprecated.rst +++ /dev/null @@ -1,5 +0,0 @@ -- **Deprecated:** - the non boolean `if g then t else e` syntax. - Use `if g is then t else e` instead - (`#22123 `_, - by Pierre Roux). diff --git a/doc/changelog/02-specification-language/22124-if-printing-Removed.rst b/doc/changelog/02-specification-language/22124-if-printing-Removed.rst deleted file mode 100644 index be8b43a4ead1..000000000000 --- a/doc/changelog/02-specification-language/22124-if-printing-Removed.rst +++ /dev/null @@ -1,4 +0,0 @@ -- **Removed:** - table ``Printing If`` - (`#22124 `_, - by Pierre Roux). diff --git a/doc/changelog/02-specification-language/22170-belowtype-Fixed.rst b/doc/changelog/02-specification-language/22170-belowtype-Fixed.rst deleted file mode 100644 index c477249841a0..000000000000 --- a/doc/changelog/02-specification-language/22170-belowtype-Fixed.rst +++ /dev/null @@ -1,6 +0,0 @@ -- **Fixed:** - when a sort variables is constrained with `Prop <= q` but does not require `q <= Type`, - it will be collapsed to `Prop` instead of `Type` - (`#22170 `_, - fixes `#22152 `_, - by Gaëtan Gilbert). diff --git a/doc/changelog/02-specification-language/22207-record-with-Added.rst b/doc/changelog/02-specification-language/22207-record-with-Added.rst deleted file mode 100644 index 83fb4f7fced7..000000000000 --- a/doc/changelog/02-specification-language/22207-record-with-Added.rst +++ /dev/null @@ -1,5 +0,0 @@ -- **Added:** - :n:`%{| @term1 with @record_declaration |%}` to provide default values for omitted fields in a record value - (`#22207 `_, - fixes `#14438 `_, - by Gaëtan Gilbert and Clément Pit-Claudel). diff --git a/doc/changelog/03-notations/21671-binder-constr-Changed.rst b/doc/changelog/03-notations/21671-binder-constr-Changed.rst deleted file mode 100644 index ff1345cf574f..000000000000 --- a/doc/changelog/03-notations/21671-binder-constr-Changed.rst +++ /dev/null @@ -1,34 +0,0 @@ -- **Changed:** - Until 8.19 term level 200 contained a sub-entry `binder_constr` - (containing e.g. `forall`) and notations declared at level 200 were - redirected to `binder_constr`. In 8.19 `binder_constr` was moved to - level 10, keeping the redirection for notations declared at level 200. - - `binder_constr` has now been removed with its parsing rules put - directly at level 10, and non left recursive notations declared at - level 200 are redirected to level 10. Any right recursion in such a - redirected notation is still interpreted as though it was really in - right associative level 200, i.e. the right recursion is at - level 200. Left recursive notations are not redirected. - - The redirection will be removed in the future and is therefore - deprecated. To keep the current behaviour, declare your notations at - level 10 and any recursion at level 200. For instance, - - .. rocqdoc:: - - Reserved Notation "'exists' x .. y , p" - (at level 200, x binder). - - becomes - - .. rocqdoc:: - - Reserved Notation "'exists' x .. y , p" - (at level 10, x binder, p at level 200). - - Finally note that any `associativity` annotation on notations - declared at level 200 are currrently ignored to avoid interfering - with the redirection to left-associative level 10 (`#21671 - `_, by Gaëtan - Gilbert). diff --git a/doc/changelog/03-notations/22194-master-Added.rst b/doc/changelog/03-notations/22194-master-Added.rst deleted file mode 100644 index 7ecb7ef34765..000000000000 --- a/doc/changelog/03-notations/22194-master-Added.rst +++ /dev/null @@ -1,4 +0,0 @@ -- **Added:** - Print the location a notation was defined (and where it was reserved) when using `Locate` - (`#22194 `_, - by Johannes Hostert). diff --git a/doc/changelog/04-tactics/20175-janno-unif-red-prim.rst b/doc/changelog/04-tactics/20175-janno-unif-red-prim.rst deleted file mode 100644 index a6a4e9370b65..000000000000 --- a/doc/changelog/04-tactics/20175-janno-unif-red-prim.rst +++ /dev/null @@ -1,6 +0,0 @@ -- **Fixed:** - Support primitive operations in old and new unification - (`#20175 `_, - fixes `#18259 `_ - and `#20155 `_, - by Jan-Oliver Kaiser). diff --git a/doc/changelog/04-tactics/21521-strat-pattern-ltac-Added.rst b/doc/changelog/04-tactics/21521-strat-pattern-ltac-Added.rst deleted file mode 100644 index 7815d5c8d411..000000000000 --- a/doc/changelog/04-tactics/21521-strat-pattern-ltac-Added.rst +++ /dev/null @@ -1,5 +0,0 @@ -- **Added:** - Add :n:`matches` and :n:`tactic` :ref:`strategies ` - to :tacn:`rewrite_strat` for :ref:`Ltac1 ` and :ref:`Ltac2 ` tactics - (`#21521 `_, - by Matthieu Sozeau and Mathis Bouverot-Dupuis). diff --git a/doc/changelog/04-tactics/21631-stop-zeta-rewrite-Changed.rst b/doc/changelog/04-tactics/21631-stop-zeta-rewrite-Changed.rst deleted file mode 100644 index 4d950665245b..000000000000 --- a/doc/changelog/04-tactics/21631-stop-zeta-rewrite-Changed.rst +++ /dev/null @@ -1,5 +0,0 @@ -- **Changed:** - Stop zeta-normalizing generalized rewriting proofs for better - sharing and performance - (`#21631 `_, - by Matthieu Sozeau). diff --git a/doc/changelog/04-tactics/21676-constr-quotation-abstract-no-inline-Changed.rst b/doc/changelog/04-tactics/21676-constr-quotation-abstract-no-inline-Changed.rst deleted file mode 100644 index eedbb8da8c38..000000000000 --- a/doc/changelog/04-tactics/21676-constr-quotation-abstract-no-inline-Changed.rst +++ /dev/null @@ -1,7 +0,0 @@ -- **Changed:** - :tacn:`abstract`-ed subproofs within tactic quotations are not - inlined any more. The previous behavior can be restored through - the deprecated :flag:`Inline Abstract Subproof` flag - (`#21676 `_, - fixes `#7905 `_, - by Pierre-Marie Pédrot). diff --git a/doc/changelog/04-tactics/21811-genScheme-Changed.rst b/doc/changelog/04-tactics/21811-genScheme-Changed.rst deleted file mode 100644 index 4c449063cdba..000000000000 --- a/doc/changelog/04-tactics/21811-genScheme-Changed.rst +++ /dev/null @@ -1,5 +0,0 @@ -- **Changed:** - Generalize DeclareScheme to be able to register schemes for any GlobRef, - and not just for inductive types - (`#21811 `_, - by Thomas Lamiaux). diff --git a/doc/changelog/04-tactics/21833-rm-non-global-hint-Removed.rst b/doc/changelog/04-tactics/21833-rm-non-global-hint-Removed.rst deleted file mode 100644 index 0b445b8223e2..000000000000 --- a/doc/changelog/04-tactics/21833-rm-non-global-hint-Removed.rst +++ /dev/null @@ -1,5 +0,0 @@ -- **Removed:** - the ability to use non-reference hints in `using` clauses - of :tacn:`auto`-like tactics - (`#21833 `_, - by Pierre-Marie Pédrot). diff --git a/doc/changelog/04-tactics/21862-cleanup-hints-globref-Changed.rst b/doc/changelog/04-tactics/21862-cleanup-hints-globref-Changed.rst deleted file mode 100644 index 13972b158b31..000000000000 --- a/doc/changelog/04-tactics/21862-cleanup-hints-globref-Changed.rst +++ /dev/null @@ -1,9 +0,0 @@ -- **Changed:** - hints from a functor argument whose underlying reference is - marked Inline in the functor parameter type are not expanded - into their inlined value anymore at application time. This - prevents arbitrary terms from flowing into hint databases. - This change is not backwards compatible but breakage should - be extremely uncommon - (`#21862 `_, - by Pierre-Marie Pédrot). diff --git a/doc/changelog/04-tactics/21928-arrayall-Changed.rst b/doc/changelog/04-tactics/21928-arrayall-Changed.rst deleted file mode 100644 index 23af292eb2ab..000000000000 --- a/doc/changelog/04-tactics/21928-arrayall-Changed.rst +++ /dev/null @@ -1,4 +0,0 @@ -- **Changed:** - Extend generation of eliminators to handle nesting with Primitive Arrays - (`#21928 `_, - by Léo Soudant). diff --git a/doc/changelog/04-tactics/21987-context-secvar-Changed.rst b/doc/changelog/04-tactics/21987-context-secvar-Changed.rst deleted file mode 100644 index 5f8714bf4b94..000000000000 --- a/doc/changelog/04-tactics/21987-context-secvar-Changed.rst +++ /dev/null @@ -1,5 +0,0 @@ -- **Changed:** - :tacn:`clear` checks that identifiers are bound even when they are ltac variables - (typically in `match goal with H : _ |- _ => foo H; clear H end`, `clear` now fails if `foo` cleared H where before it would succeed without doing anything) - (`#21987 `_, - by Gaëtan Gilbert). diff --git a/doc/changelog/04-tactics/21987-context-secvar-Fixed.rst b/doc/changelog/04-tactics/21987-context-secvar-Fixed.rst deleted file mode 100644 index 58be0ef1c22a..000000000000 --- a/doc/changelog/04-tactics/21987-context-secvar-Fixed.rst +++ /dev/null @@ -1,11 +0,0 @@ -- **Fixed:** - the proof engine now keeps track of which hypotheses are section variables - instead of assuming that a variable sharing a name with a section variable is a section variable. - In particular :tacn:`destruct` now clears non-section-variable variables which share a name with a section variable. - Note that modifying a section variable (e.g. with `apply in`) makes it a non-section-variable - (`#21987 `_, - fixes `#18858 `_ - and `#12304 `_ - and `#11487 `_ - and `#6773 `_, - by Gaëtan Gilbert). diff --git a/doc/changelog/04-tactics/22001-gene-eqs-vars-Changed.rst b/doc/changelog/04-tactics/22001-gene-eqs-vars-Changed.rst deleted file mode 100644 index a0ff941c6401..000000000000 --- a/doc/changelog/04-tactics/22001-gene-eqs-vars-Changed.rst +++ /dev/null @@ -1,6 +0,0 @@ -- **Changed:** - :tacn:`generalize_eqs_vars` (used in :tacn:`dependent induction`) - does less useless generalizations - (`#22001 `_, - fixes `#22000 `_, - by Gaëtan Gilbert). diff --git a/doc/changelog/04-tactics/22154-fix-rec-Fixed.rst b/doc/changelog/04-tactics/22154-fix-rec-Fixed.rst deleted file mode 100644 index 6839ee0f95ea..000000000000 --- a/doc/changelog/04-tactics/22154-fix-rec-Fixed.rst +++ /dev/null @@ -1,5 +0,0 @@ -- **Fixed:** - Fix generation of eliminators for not recursive inductive types but with non-uniform parameters - (`#22154 `_, - fixes `#22149 `_, - by Thomas Lamiaux). diff --git a/doc/changelog/04-tactics/22182-clear-shelf-Fixed.rst b/doc/changelog/04-tactics/22182-clear-shelf-Fixed.rst deleted file mode 100644 index 405af5f3539a..000000000000 --- a/doc/changelog/04-tactics/22182-clear-shelf-Fixed.rst +++ /dev/null @@ -1,6 +0,0 @@ -- **Fixed:** - :tacn:`clear` does not unshelve previously shelved evars - (`#22182 `_, - fixes `#22076 `_ - and `#21831 `_, - by Gaëtan Gilbert). diff --git a/doc/changelog/04-tactics/22184-master-Changed.rst b/doc/changelog/04-tactics/22184-master-Changed.rst deleted file mode 100644 index bcb8dd2c7e0f..000000000000 --- a/doc/changelog/04-tactics/22184-master-Changed.rst +++ /dev/null @@ -1,5 +0,0 @@ -- **Changed:** - The autorewrite tactic now accepts a direction: `autorewrite <- with xyz` - reverses the direction of rewriting rules registered in `xyz` (`#22184 - `_, fixes `#1875 - `_, by Clément Pit-Claudel). diff --git a/doc/changelog/04-tactics/22251-underp-proof-with-Changed.rst b/doc/changelog/04-tactics/22251-underp-proof-with-Changed.rst deleted file mode 100644 index ac80a1ad7fea..000000000000 --- a/doc/changelog/04-tactics/22251-underp-proof-with-Changed.rst +++ /dev/null @@ -1,4 +0,0 @@ -- **Changed:** - `...` (:cmd:`Proof with`) is not deprecated anymore and is expected to remain available - (`#22251 `_, - by Gaëtan Gilbert). diff --git a/doc/changelog/06-Ltac2-language/21542-ltac2-scoped-notations-Added.rst b/doc/changelog/06-Ltac2-language/21542-ltac2-scoped-notations-Added.rst deleted file mode 100644 index b1e4375e1bee..000000000000 --- a/doc/changelog/06-Ltac2-language/21542-ltac2-scoped-notations-Added.rst +++ /dev/null @@ -1,7 +0,0 @@ -- **Added:** - scopes for :cmd:`Ltac2 Notation` to pick the interpretation at (Ltac2) typechecking time instead of parsing time, - similar to term notation scopes - (`#21542 `_, - fixes `#16538 `_ - and `#17330 `_, - by Gaëtan Gilbert). diff --git a/doc/changelog/06-Ltac2-language/21558-ltac2-transparent-state-Added.rst b/doc/changelog/06-Ltac2-language/21558-ltac2-transparent-state-Added.rst deleted file mode 100644 index e96bc2524591..000000000000 --- a/doc/changelog/06-Ltac2-language/21558-ltac2-transparent-state-Added.rst +++ /dev/null @@ -1,6 +0,0 @@ -- **Added:** - Low-level operations to manipulate transparent states: - 1. Set-like operations (union, intersection, difference). - 2. Operations to add/remove/test membership of constants, variables, and primitive projections. - (`#21558 `_, - by Mathis Bouverot-Dupuis). diff --git a/doc/changelog/06-Ltac2-language/21617-tac2abbrev-up-Added.rst b/doc/changelog/06-Ltac2-language/21617-tac2abbrev-up-Added.rst deleted file mode 100644 index c72827fd2bd5..000000000000 --- a/doc/changelog/06-Ltac2-language/21617-tac2abbrev-up-Added.rst +++ /dev/null @@ -1,6 +0,0 @@ -- **Added:** - :cmd:`Ltac2 Abbreviation` typecheck the body at declaration time instead of when they are used. - This means incorrect abbreviations produce errors at declaration time, and also means quotations may be used inside abbreviations - (e.g. `Ltac2 Abbreviation foo := @foo.`) - (`#21617 `_, - by Gaëtan Gilbert). diff --git a/doc/changelog/06-Ltac2-language/21642-redoer-goals-Added.rst b/doc/changelog/06-Ltac2-language/21642-redoer-goals-Added.rst deleted file mode 100644 index 2c0f3a767fcf..000000000000 --- a/doc/changelog/06-Ltac2-language/21642-redoer-goals-Added.rst +++ /dev/null @@ -1,5 +0,0 @@ -- **Added:** - `Ltac2.Control.reorder_goals` - (`#21642 `_, - fixes `#20087 `_, - by Gaëtan Gilbert). diff --git a/doc/changelog/06-Ltac2-language/21658-ltac2-scheme-lookup-Added.rst b/doc/changelog/06-Ltac2-language/21658-ltac2-scheme-lookup-Added.rst deleted file mode 100644 index b90f492724a5..000000000000 --- a/doc/changelog/06-Ltac2-language/21658-ltac2-scheme-lookup-Added.rst +++ /dev/null @@ -1,5 +0,0 @@ -- **Added:** - ``Scheme.lookup`` in Ltac2 to look up registered inductive schemes - (elimination, case analysis, etc.) by scheme kind (`#21658 - `_, fixes `#20987 - `_, by Jason Gross). diff --git a/doc/changelog/06-Ltac2-language/21762-ltac2-strategy-Added.rst b/doc/changelog/06-Ltac2-language/21762-ltac2-strategy-Added.rst deleted file mode 100644 index ae441c3f1b1e..000000000000 --- a/doc/changelog/06-Ltac2-language/21762-ltac2-strategy-Added.rst +++ /dev/null @@ -1,6 +0,0 @@ -- **Added:** - :tacn:`with_strategy` to Ltac2, to allow temporarily changing the strategy - level of constants during tactic execution, with automatic restoration - afterward - (`#21762 `_, - by Jason Gross). diff --git a/doc/changelog/06-Ltac2-language/21819-janno-ltac2-syntax-Added.rst b/doc/changelog/06-Ltac2-language/21819-janno-ltac2-syntax-Added.rst deleted file mode 100644 index 02d2317d23a0..000000000000 --- a/doc/changelog/06-Ltac2-language/21819-janno-ltac2-syntax-Added.rst +++ /dev/null @@ -1,4 +0,0 @@ -- **Added:** - Add OCaml-inspired `@@` and `|>` notations - (`#21819 `_, - by Jan-Oliver Kaiser). diff --git a/doc/changelog/06-Ltac2-language/21881-sprop-case-scheme-Added.rst b/doc/changelog/06-Ltac2-language/21881-sprop-case-scheme-Added.rst deleted file mode 100644 index f4f1a7c76272..000000000000 --- a/doc/changelog/06-Ltac2-language/21881-sprop-case-scheme-Added.rst +++ /dev/null @@ -1,6 +0,0 @@ -- **Added:** - ``Scheme.scase_dep`` and ``Scheme.scase_nodep`` in Ltac2 for SProp case - analysis scheme kinds, and support for registering SProp case schemes via the - ``Scheme`` command - (`#21881 `_, - by Jason Gross). diff --git a/doc/changelog/06-Ltac2-language/22092-ltac2-match-level-Changed.rst b/doc/changelog/06-Ltac2-language/22092-ltac2-match-level-Changed.rst deleted file mode 100644 index 40cc44085b92..000000000000 --- a/doc/changelog/06-Ltac2-language/22092-ltac2-match-level-Changed.rst +++ /dev/null @@ -1,4 +0,0 @@ -- **Changed:** - Parse ``match`` expressions at level 0 instead of level 5 - (`#22092 `_, - by Rodolphe Lepigre). diff --git a/doc/changelog/07-ssreflect/21478-ssreflect-rw-Changed.rst b/doc/changelog/07-ssreflect/21478-ssreflect-rw-Changed.rst deleted file mode 100644 index 82bf5fe59af0..000000000000 --- a/doc/changelog/07-ssreflect/21478-ssreflect-rw-Changed.rst +++ /dev/null @@ -1,12 +0,0 @@ -- **Changed:** - ``rewrite`` tactic for ``rw``. Since this was the major cause of - conflict with legacy tactics, ssreflect can now be loaded with less - conflicts through ``From Corelib Require Import ssreflect_rw.``. - For backward compatibility - ``From Corelib Require Import ssreflect.`` - still loads a ``rewrite`` wrapper to ``rw`` as well as the - ``if is then else `` - and ``if isn't then else `` - syntactic sugars for match - (`#21478 `_, - by Pierre Roux). diff --git a/doc/changelog/07-ssreflect/21611-of-ampersand-of-Removed.rst b/doc/changelog/07-ssreflect/21611-of-ampersand-of-Removed.rst deleted file mode 100644 index c2b0d6113d31..000000000000 --- a/doc/changelog/07-ssreflect/21611-of-ampersand-of-Removed.rst +++ /dev/null @@ -1,5 +0,0 @@ -- **Removed:** - the `of T` syntax for anonymous binders outside of constructors, - use `& T` instead - (`#21611 `_, - by Pierre Roux). diff --git a/doc/changelog/07-ssreflect/22096-fix-ssr-univpoly-Fixed.rst b/doc/changelog/07-ssreflect/22096-fix-ssr-univpoly-Fixed.rst deleted file mode 100644 index 633bc2d48147..000000000000 --- a/doc/changelog/07-ssreflect/22096-fix-ssr-univpoly-Fixed.rst +++ /dev/null @@ -1,6 +0,0 @@ -- **Fixed:** - Handling of universe polymorphism by ssrmatching (e.g. :tacn:`unlock` and :tacn:`rw` tactics), - now recording appropriate universe unifications. - (`#22096 `_, - fixes `#22086 `_, - by Matthieu Sozeau). diff --git a/doc/changelog/07-ssreflect/22169-fix-22158-Fixed.rst b/doc/changelog/07-ssreflect/22169-fix-22158-Fixed.rst deleted file mode 100644 index da95a3398e78..000000000000 --- a/doc/changelog/07-ssreflect/22169-fix-22158-Fixed.rst +++ /dev/null @@ -1,5 +0,0 @@ -- **Fixed:** - Ssreflect generalization through views in presence of universe polymorphism - (`#22169 `_, - fixes `#22158 `_, - by Matthieu Sozeau). diff --git a/doc/changelog/08-vernac-commands-and-options/17266-alloc-limit-Added.rst b/doc/changelog/08-vernac-commands-and-options/17266-alloc-limit-Added.rst deleted file mode 100644 index f29eb052248a..000000000000 --- a/doc/changelog/08-vernac-commands-and-options/17266-alloc-limit-Added.rst +++ /dev/null @@ -1,4 +0,0 @@ -- **Added:** - :cmd:`AllocLimit` and :tacn:`alloc_limit` to enforce allocation limits during execution - (`#17266 `_, - by Gaëtan Gilbert). diff --git a/doc/changelog/08-vernac-commands-and-options/20660-search-fuzzy-Added.rst b/doc/changelog/08-vernac-commands-and-options/20660-search-fuzzy-Added.rst deleted file mode 100644 index 71d628555663..000000000000 --- a/doc/changelog/08-vernac-commands-and-options/20660-search-fuzzy-Added.rst +++ /dev/null @@ -1,5 +0,0 @@ -- **Added:** - approximate matching in :cmd:`Search`, controlled by new option :opt:`Fuzzy Search`. - Currently only when searching by name (:n:`Search @string`) - (`#20660 `_, - by Gaëtan Gilbert). diff --git a/doc/changelog/08-vernac-commands-and-options/21473-fix-printing-Fixed.rst b/doc/changelog/08-vernac-commands-and-options/21473-fix-printing-Fixed.rst deleted file mode 100644 index 41ac55a7ed7d..000000000000 --- a/doc/changelog/08-vernac-commands-and-options/21473-fix-printing-Fixed.rst +++ /dev/null @@ -1,5 +0,0 @@ -- **Fixed:** fallback printing of inductives using - ```` now prints correctly - (though with possibly more qualification than needed) - (it should in any case only happen rarely from module errors) - (`#21484 `_, by Gaëtan Gilbert). diff --git a/doc/changelog/08-vernac-commands-and-options/21578-fix-induction-scheme-sprop-Fixed.rst b/doc/changelog/08-vernac-commands-and-options/21578-fix-induction-scheme-sprop-Fixed.rst deleted file mode 100644 index 6ab77ba393bd..000000000000 --- a/doc/changelog/08-vernac-commands-and-options/21578-fix-induction-scheme-sprop-Fixed.rst +++ /dev/null @@ -1,6 +0,0 @@ -- **Fixed:** The default name of the induction principle in :g:`SProp` - generated by :g:`Scheme Induction for T Sort SProp` is now correct. It is now - :g:`T_sind`, instead of :g:`T_inds`. Similarly for :g:`Case`, the name will - now be :g:`T_scase` instead of :g:`T_cases`. - (`#21578 `_, - by Jean Caspar). diff --git a/doc/changelog/08-vernac-commands-and-options/21626-noverbose-Removed.rst b/doc/changelog/08-vernac-commands-and-options/21626-noverbose-Removed.rst deleted file mode 100644 index 8ae1234f6166..000000000000 --- a/doc/changelog/08-vernac-commands-and-options/21626-noverbose-Removed.rst +++ /dev/null @@ -1,7 +0,0 @@ -- **Removed:** - `-verbose` and `load-vernac-source-verbose` (`-lv`). - `-verbose` has been ignored for several versions. - `-lv` would print the input file (as-is from source, not pretty printed) - which does not seem useful - (`#21626 `_, - by Gaëtan Gilbert). diff --git a/doc/changelog/08-vernac-commands-and-options/21645-print-regular-match-Added.rst b/doc/changelog/08-vernac-commands-and-options/21645-print-regular-match-Added.rst deleted file mode 100644 index d344628c80bb..000000000000 --- a/doc/changelog/08-vernac-commands-and-options/21645-print-regular-match-Added.rst +++ /dev/null @@ -1,4 +0,0 @@ -- **Added:** - flag :flag:`Printing Regular Matches` to disable alternate match syntaxes - (`#21645 `_, - by Gaëtan Gilbert). diff --git a/doc/changelog/08-vernac-commands-and-options/21779-set-indices-matter-Added.rst b/doc/changelog/08-vernac-commands-and-options/21779-set-indices-matter-Added.rst deleted file mode 100644 index 5ebaf28a94c9..000000000000 --- a/doc/changelog/08-vernac-commands-and-options/21779-set-indices-matter-Added.rst +++ /dev/null @@ -1,6 +0,0 @@ -- **Added:** - flag :flag:`Indices Matter` to set ``-indices-matter`` locally, - controlling whether the types of indices of inductive types - contribute universe constraints - (`#21779 `_, - by Jason Gross). diff --git a/doc/changelog/08-vernac-commands-and-options/21823-genAbout-Changed.rst b/doc/changelog/08-vernac-commands-and-options/21823-genAbout-Changed.rst deleted file mode 100644 index 23dabd266def..000000000000 --- a/doc/changelog/08-vernac-commands-and-options/21823-genAbout-Changed.rst +++ /dev/null @@ -1,4 +0,0 @@ -- **Changed:** - Generalize `About` to be able to handle several definitions at once - (`#21823 `_, - by Thomas Lamiaux). diff --git a/doc/changelog/08-vernac-commands-and-options/21825-print-assumptions-globals-types-Fixed.rst b/doc/changelog/08-vernac-commands-and-options/21825-print-assumptions-globals-types-Fixed.rst deleted file mode 100644 index f3852f52da28..000000000000 --- a/doc/changelog/08-vernac-commands-and-options/21825-print-assumptions-globals-types-Fixed.rst +++ /dev/null @@ -1,6 +0,0 @@ -- **Fixed:** - :cmd:`Print Assumptions` now also traverses the types of global - definitions, not just their bodies, to detect dependencies on axioms - that appear only in the type - (`#21825 `_, - by Jason Gross). diff --git a/doc/changelog/08-vernac-commands-and-options/21865-warn-missing-proof-Added.rst b/doc/changelog/08-vernac-commands-and-options/21865-warn-missing-proof-Added.rst deleted file mode 100644 index 39bf234415e0..000000000000 --- a/doc/changelog/08-vernac-commands-and-options/21865-warn-missing-proof-Added.rst +++ /dev/null @@ -1,4 +0,0 @@ -- **Added:** - warning when an interactive proof is not started by :cmd:`Proof`, and error when :cmd:`Proof` is used multiple times or is used after a tactic has been used - (`#21865 `_, - by Gaëtan Gilbert). diff --git a/doc/changelog/08-vernac-commands-and-options/21867-pr-debug-delta-resolver-Added.rst b/doc/changelog/08-vernac-commands-and-options/21867-pr-debug-delta-resolver-Added.rst deleted file mode 100644 index 1af8325f62c1..000000000000 --- a/doc/changelog/08-vernac-commands-and-options/21867-pr-debug-delta-resolver-Added.rst +++ /dev/null @@ -1,5 +0,0 @@ -- **Added:** - a `Print Debug Delta` vernacular command to print debug - information about module delta-resolvers - (`#21867 `_, - by Pierre-Marie Pédrot). diff --git a/doc/changelog/08-vernac-commands-and-options/21934-print-flat-Added.rst b/doc/changelog/08-vernac-commands-and-options/21934-print-flat-Added.rst deleted file mode 100644 index 9b4445d8f32a..000000000000 --- a/doc/changelog/08-vernac-commands-and-options/21934-print-flat-Added.rst +++ /dev/null @@ -1,4 +0,0 @@ -- **Added:** - :cmd:`Print Grammar` with argument `Tree` to print the factorizations done by the grammar engine - (`#21934 `_, - by Gaëtan Gilbert). diff --git a/doc/changelog/08-vernac-commands-and-options/21947-asymmetric-patterns-no-implicits-Changed.rst b/doc/changelog/08-vernac-commands-and-options/21947-asymmetric-patterns-no-implicits-Changed.rst deleted file mode 100644 index 179d430365c2..000000000000 --- a/doc/changelog/08-vernac-commands-and-options/21947-asymmetric-patterns-no-implicits-Changed.rst +++ /dev/null @@ -1,8 +0,0 @@ -- **Changed:** - the behavior of the :flag:`Asymmetric Patterns` flag, which no - longer disactivates implicit arguments in patterns. Set the - compatibility flag :flag:`Asymmetric Patterns No Implicits` to - retrieve the previous behavior - (`#21947 `_, - fixes `#21769 `_, - by Pierre Roux). diff --git a/doc/changelog/08-vernac-commands-and-options/22017-GeneralizePrint-Changed.rst b/doc/changelog/08-vernac-commands-and-options/22017-GeneralizePrint-Changed.rst deleted file mode 100644 index 3545344f864c..000000000000 --- a/doc/changelog/08-vernac-commands-and-options/22017-GeneralizePrint-Changed.rst +++ /dev/null @@ -1,4 +0,0 @@ -- **Changed:** - Generalize Print command to print multiples definitions - (`#22017 `_, - by Elsa Rabu). diff --git a/doc/changelog/08-vernac-commands-and-options/22107-keep-using-Added.rst b/doc/changelog/08-vernac-commands-and-options/22107-keep-using-Added.rst deleted file mode 100644 index 452d2f842484..000000000000 --- a/doc/changelog/08-vernac-commands-and-options/22107-keep-using-Added.rst +++ /dev/null @@ -1,4 +0,0 @@ -- **Added:** - :flag:`Proof Using Clear Unused` which automatically clears variables not allowed by a :cmd:`Proof using` annotation at the beginning of an interactive proof - (`#22107 `_, - by Gaëtan Gilbert). diff --git a/doc/changelog/08-vernac-commands-and-options/22193-blacklist-search-table-Added.rst b/doc/changelog/08-vernac-commands-and-options/22193-blacklist-search-table-Added.rst deleted file mode 100644 index cd0407d85ced..000000000000 --- a/doc/changelog/08-vernac-commands-and-options/22193-blacklist-search-table-Added.rst +++ /dev/null @@ -1,5 +0,0 @@ -- **Added:** - The Search Blacklist table now accepts plain references, that - are excluded from the Search results - (`#22193 `_, - by Pierre-Marie Pédrot). diff --git a/doc/changelog/08-vernac-commands-and-options/22231-coqdep-warn-loc-Changed.rst b/doc/changelog/08-vernac-commands-and-options/22231-coqdep-warn-loc-Changed.rst deleted file mode 100644 index cf743b1d9596..000000000000 --- a/doc/changelog/08-vernac-commands-and-options/22231-coqdep-warn-loc-Changed.rst +++ /dev/null @@ -1,5 +0,0 @@ -- **Changed:** - `rocq dep` errors have more readable locations, and warnings have locations - (`#22231 `_, - fixes `#10815 `_, - by Gaëtan Gilbert). diff --git a/doc/changelog/09-cli-tools/21423-rocq-wc-Proof-Fixed.rst b/doc/changelog/09-cli-tools/21423-rocq-wc-Proof-Fixed.rst deleted file mode 100644 index 7286abe00b17..000000000000 --- a/doc/changelog/09-cli-tools/21423-rocq-wc-Proof-Fixed.rst +++ /dev/null @@ -1,5 +0,0 @@ -- **Fixed:** - ``rocq wc`` now handles tactics containing the word ``Proof`` correctly. - (`#21423 `_, - fixes `#21422 `_, - by Johannes Hostert). diff --git a/doc/changelog/09-cli-tools/21950-coqdoc-alectryon-Added.rst b/doc/changelog/09-cli-tools/21950-coqdoc-alectryon-Added.rst deleted file mode 100644 index d366b665b11b..000000000000 --- a/doc/changelog/09-cli-tools/21950-coqdoc-alectryon-Added.rst +++ /dev/null @@ -1,4 +0,0 @@ -- **Added:** - New Alectryon Markdown backend for `rocq doc` - (`#21950 `_, - by Dario Halilovic). diff --git a/doc/changelog/11-corelib/21971-number-nota-Changed.rst b/doc/changelog/11-corelib/21971-number-nota-Changed.rst deleted file mode 100644 index 4ce3ec400b94..000000000000 --- a/doc/changelog/11-corelib/21971-number-nota-Changed.rst +++ /dev/null @@ -1,4 +0,0 @@ -- **Changed:** - number notations for `nat` `Number.int` and `Number.uint` are now declared in `NumberNotations` submodules of `Nat` and `Number`. The submodules are exported from `Nat` and `Number` (which are not imported by default) and from `Prelude` (which is imported by default) so visible changes should be rare - (`#21971 `_, - by Gaëtan Gilbert). diff --git a/doc/changelog/11-corelib/22221-template-scheme-univs-Fixed.rst b/doc/changelog/11-corelib/22221-template-scheme-univs-Fixed.rst deleted file mode 100644 index 636a22f0deae..000000000000 --- a/doc/changelog/11-corelib/22221-template-scheme-univs-Fixed.rst +++ /dev/null @@ -1,13 +0,0 @@ -- **Fixed:** - Rewriting schemes over template polymorphic inductive types - (generated by :cmd:`Scheme` ``Rewriting``, or on the fly by tactics - such as :tacn:`rewrite` on user-defined equality types) no longer - mention the global template universes in their types. In - particular, the types of ``eq_sym``, ``eq_sym_involutive`` and - ``eq_rew_r_dep`` now use a universe local to the scheme instead of - ``eq.u0``, so that using these constants no longer adds constraints - on ``eq.u0`` (which is deprecated, see the ``bad-template-constraint`` - warning) - (`#22221 `_, - fixes `#22220 `_, - by Jason Gross). diff --git a/doc/changelog/12-infrastructure-and-dependencies/21564-package-Added.rst b/doc/changelog/12-infrastructure-and-dependencies/21564-package-Added.rst deleted file mode 100644 index 34e75eb4dbd0..000000000000 --- a/doc/changelog/12-infrastructure-and-dependencies/21564-package-Added.rst +++ /dev/null @@ -1,13 +0,0 @@ -- **Added:** - New notion of Rocq package and installation layout supported by a new - command-line option ``-package DEP`` that automatically adds the correct - ``-Q`` and ``-I`` options for ``DEP`` and its transitive dependencies. - For backwards compatibility, the old installation scheme targeting the - ``coq/user-contrib`` directory is kept, but the plan is to remove it - after packages have been ported to the new installation scheme. - The ``rocq makefile`` command can be made to rely on the new installation - scheme by passing the ``--rocq-package PKGNAME`` argument, and optionally - the ``--legacy-support`` argument to also install using the legacy - installation scheme - (`#21564 `_, - by Rodolphe Lepigre). diff --git a/doc/changelog/12-infrastructure-and-dependencies/21660-recent-dune-Changed.rst b/doc/changelog/12-infrastructure-and-dependencies/21660-recent-dune-Changed.rst deleted file mode 100644 index a577897ba219..000000000000 --- a/doc/changelog/12-infrastructure-and-dependencies/21660-recent-dune-Changed.rst +++ /dev/null @@ -1,4 +0,0 @@ -- **Changed:** - Require ``dune`` version 3.21.0 to support the ``rocq.theory`` stanza - (`#21660 `_, - by Rodolphe Lepigre). diff --git a/doc/changelog/12-infrastructure-and-dependencies/22198-relative-if-dune-Fixed.rst b/doc/changelog/12-infrastructure-and-dependencies/22198-relative-if-dune-Fixed.rst deleted file mode 100644 index d069e876ebe7..000000000000 --- a/doc/changelog/12-infrastructure-and-dependencies/22198-relative-if-dune-Fixed.rst +++ /dev/null @@ -1,5 +0,0 @@ -- **Fixed:** - building Rocq on Windows with Dune 3.24 or later - (path normalization in custom Rocq rules went awry) - (`#22198 `_, - by Gaëtan Gilbert). diff --git a/doc/changelog/14-misc/21852-warnerror-legacy-loading-Removed.rst b/doc/changelog/14-misc/21852-warnerror-legacy-loading-Removed.rst deleted file mode 100644 index 561da3291ae0..000000000000 --- a/doc/changelog/14-misc/21852-warnerror-legacy-loading-Removed.rst +++ /dev/null @@ -1,6 +0,0 @@ -- **Removed:** - legacy loading mode for plugins, that was deprecated in Rocq 9.0. - To adapt, change your ``Declare ML Module "legacy:current".`` - to ``Declare ML Module "current".`` - (`#21852 `_, - by Pierre Roux). diff --git a/doc/sphinx/changes.rst b/doc/sphinx/changes.rst index e5baacbc3f49..cdaa91b80fbe 100644 --- a/doc/sphinx/changes.rst +++ b/doc/sphinx/changes.rst @@ -8,6 +8,645 @@ Recent changes .. include:: ../unreleased.rst +Version 9.3 +----------- + +.. contents:: + :local: + :depth: 1 + +Summary of changes +~~~~~~~~~~~~~~~~~~ + +We highlight some of the most impactful changes here: + +- :ref:`require dune version 3.21.0<93dune321>` to support the ``rocq.theory`` stanza +- new :ref:`notion of Rocq package<93package>` and installation layout supported by a new + command-line option ``-package DEP`` that automatically adds the correct + ``-Q`` options for ``DEP`` and its transitive dependencies. + For backwards compatibility, the old installation scheme targeting the + ``coq/user-contrib`` directory is kept (see also + :ref:`Rocq makefile ` documentation for ``--rocq-package``) +- new syntactic sugar ``{| t with n := v |}`` to provide default values for + :ref:`omitted fields in a record value<93recordupdate>` +- new OCaml-inspired `@@` and `|>` :ref:`notations in Ltac2<93ltac2not>` +- new syntactic sugar for :ref:`match with one interesting case<93syntaxifte>`. For + example `if g is c then t else e` stands for + `match g with c => t | _ => e end` + (see :ref:`if-then-else`) +- new syntactic sugars `& T` for :ref:`anonymous binders<93anonymbinder>` `(_ : T)` + and `of T & ... & T` for anonymous binders in constructors, enabling + `Variant t := C1 of a & b & c | C2 x y of P x & Q y.` +- SSReflect :tacn:`rewrite` tactic renamed into :ref:`rw<93ssrrw>`, the old name is still + available via ``Import ssreflect`` +- new :cmd:`AllocLimit` and :tacn:`alloc_limit` to enforce :ref:`allocation limits<93alloclimit>` + during execution +- :ref:`extend generation of eliminators<93elim>` to handle nesting with Primitive Arrays +- new :ref:`Alectryon Markdown backend<93alectryon>` for `rocq doc` +- :ref:`fixed confusion<93confusion>` between section variables and + goal hypotheses with the same name, which made clearing section + variables very buggy + +See the `Changes in 9.3.0`_ section below for the detailed list of changes, +including potentially breaking changes marked with **Changed**. +Rocq's `reference manual for 9.3 `_, +documentation of the 9.3 `corelib `__ +and `developer documentation of the 9.3 ML API `_ +are also available. + +Théo Zimmermann, with help from Jason Gross and Gaëtan Gilbert, maintained +`coqbot `__ used to run Rocq's CI and other +pull request management tasks. + +Jason Gross maintained the `bug minimizer `_ +and its `automatic use through coqbot `_. + +Ali Caglayan, Rudi Grinberg and Rodolphe Lepigre maintained the +`Dune build system for OCaml and Coq/Rocq `_ +used to build the Rocq Prover itself and many Rocq projects. + +The `rocq opam repository `_ for Rocq packages has been maintained by +Guillaume Claret, Guillaume Melquiond, Karl Palmskog, Matthieu Sozeau +and Enrico Tassi with contributions from many users. The up-to-date list +of packages is `available on the Rocq website `_. + +Sylvain Borgogno, Erik Martin-Dorel maintained the +`Rocq Docker images `_ and +the `docker-keeper `_ compiler +used to build and keep those images up to date (note that the tool is not Rocq specific). +Sylvain Borgogno, Erik Martin-Dorel and Théo Zimmermann maintained the +`docker-coq-action `_ +container action (which is applicable to any opam project hosted on GitHub). + +Cyril Cohen, Vincent Laporte, Pierre Roux and Théo Zimmermann +maintained the `Nix toolbox `_. +The docker-coq-action and the Nix toolbox are used by many Rocq projects for continuous integration. + +Rocq 9.3 was made possible thanks to the following 23 reviewers: +Mathis Bouverot, Cyril Cohen, Pierre Corbineau, Andres Erbsen, Jim Fehrle, +Gaëtan Gilbert, Jason Gross, Hugo Herbelin, Emilio Jesús Gallego Arias, Thomas +Lamiaux, Rodolphe Lepigre, Yann Leray, Erik Martin-Dorel, Guillaume Melquiond, +Guillaume Munch-Maccagnoni, Clément Pit-Claudel, Pierre-Marie Pédrot, Pierre +Roux, Matthieu Sozeau, Nicolas Tabareau, Enrico Tassi, Li-yao Xia, Théo +Zimmermann. + +See the `Rocq Team `_ page for +more details on Rocq's development teams. + +The 50 contributors to the 9.3 version are: +Peio Borthelle, Matteo Calosci, Elliott, Jean Caspar, Cecile Marcon, +jstrattonsmith, vblot, Mathis Bouverot-Dupuis, Julien Cretin, Tomás Díaz, Jim +Fehrle, Davide Fissore, Gaëtan Gilbert, Jason Gross, Dario Halilovic, Hugo +Herbelin, Johannes Hostert, Ralf Jung, Suraaj K S, Jan-Oliver Kaiser, Chantal +Keller, Thomas Lamiaux, Vincent Laviron, Rodolphe Lepigre, Yann Leray, +Jean-Christophe Léchenet, Gregory Malecha, Guillaume Melquiond, Daan Michiels, +Soonwon Moon, Kanghee Park, Clément Pit-Claudel, Josselin Poiret, +Pierre-Marie Pédrot, Elsa Rabu, Pierre Roux, Gabriel Scherer, Léo Soudant, +Matthieu Sozeau, Nicolas Tabareau, Enrico Tassi, Will Thomas, Théo Zimmermann, +Leonid Znamenok, Nathan van der Kamp. + +The Rocq community at large helped improve this new version via +the GitHub issue and pull request system, +the `Discourse forum `__ and the +`Rocq Zulip chat `_. + +Enrico Tassi is the release manager of Rocq 9.2. +This release is the result of 437 merged PRs, closing 65 issues. + +| Sophia-Antipolis, July 2026 +| Enrico Tassi for the Rocq development team + +Changes in 9.3.0 +~~~~~~~~~~~~~~~~ + +.. contents:: + :local: + +Kernel +^^^^^^ + +- **Changed:** + Sort-polymorphic records can now have primitive projections + with eta conversion depending on instantiation, + which is checked at runtime + (`#21416 `_, + by Tomas Diaz). +- **Changed:** + Check convertibility of the motive applied to indices instead of directly + convertibility of indices + (when :flag:`Definitional UIP` is enabled). + This is a stronger reduction rule that subsumes the previous one and is + justified by a proof using logical relations + (`#22150 `_, + by nicolas tabareau). +- **Added:** + new flag :flag:`Kernel Conversion Dep Heuristic` that enables a heuristic for + smarter constant unfolding during conversion. When enabled, if two constants + have the same strategy level (see :cmd:`Strategy`) and one constant's + definition depends on the other, the dependent constant is unfolded first. + This can significantly speed up conversions in cases like checking ``c1 = + c2`` vs ``c2 = c1`` where one definition wraps the other. The flag defaults + to off, preserving the existing behavior of preferentially unfolding the + right-hand side first (`#21514 + `_, fixes `#21509 + `_, by Jason Gross). +- **Added:** + Added support for matching on specific global sorts in rewrite rules + (`#21663 `_, + by Yann Leray). +- **Added:** + kernel now tracks reliance on ``-indices-matter`` not being passed, and + prints this information in the checker, and in :cmd:`Print Assumptions` + when ``-indices-matter`` is passed + (`#21774 `_, + by Jason Gross). +- **Fixed:** + Unsetting :flag:`Universe Checking` doesn't confuse sorts anymore, only allowing Type in Type + (`#21531 `_, + fixes `#20241 `_ + and `#20667 `_, + by Yann Leray). +- **Fixed:** + Pass the correct environment in a reduction call inside the guard checker + (`#21845 `_, + fixes `#21839 `_, + by Yann Leray). +- **Fixed:** + Fix regression that prevented some mutual fixpoints involving nested inductives + (`#21896 `_, + fixes `#21892 `_, + by Yann Leray). + +Specification language, type inference +^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ + +- **Changed:** External hints now emit a new log entry starting with "running + HINT on GOAL" before the tactic code is executed; all hints had their log entry + for a successful application changed from just "HINT on GOAL" to "applied HINT + on GOAL" (`#21899 `_, fixes + `#21898 `_, by Jan-Oliver + Kaiser). +- **Removed:** + table ``Printing If`` + (`#22124 `_, + by Pierre Roux). +- **Deprecated:** + the non boolean `if g then t else e` syntax. + Use `if g is then t else e` instead + (`#22123 `_, + by Pierre Roux). +- **Added:** + elaboration of implicit sort qualities, controlled by the flag :flag:`Collapse Sorts ToType` + (`#21450 `_, + by Tomas Diaz). + + .. _93syntaxifte: + +- **Added:** + new syntactic sugar `if g is c then t else e` + for `match g with c => t | _ => e end`. This adds the + new reserved keyword `is` + (`#21609 `_, + by Pierre Roux). + + .. _93anonymbinder: + +- **Added:** + new syntactic sugars `& T` for anonymous binders `(_ : T)` + and `of T & ... & T` for anonymous binders in constructors, enabling the + `Variant t := C1 of a & b & c | C2 x y of P x & Q y.` syntax. + This adds the new reserved keyword `of` + (`#21611 `_, + by Pierre Roux). + + .. _93recordupdate: + +- **Added:** + :n:`%{| @term1 with @record_declaration |%}` to provide default values for omitted fields in a record value + (`#22207 `_, + fixes `#14438 `_, + by Gaëtan Gilbert and Clément Pit-Claudel). +- **Fixed:** + tactic definitions (:cmd:`Ltac`, :cmd:`Ltac2`, tactic notations, etc) + correctly check that universe names are declared instead of delaying the error to when the tactic is used + (`#21627 `_, + fixes `#21616 `_, + by Gaëtan Gilbert). +- **Fixed:** + when a sort variables is constrained with `Prop <= q` but does not require `q <= Type`, + it will be collapsed to `Prop` instead of `Type` + (`#22170 `_, + fixes `#22152 `_, + by Gaëtan Gilbert). + +Notations +^^^^^^^^^ + +- **Changed:** + Until 8.19 term level 200 contained a sub-entry `binder_constr` + (containing e.g. `forall`) and notations declared at level 200 were + redirected to `binder_constr`. In 8.19 `binder_constr` was moved to + level 10, keeping the redirection for notations declared at level 200. + + `binder_constr` has now been removed with its parsing rules put + directly at level 10, and non left recursive notations declared at + level 200 are redirected to level 10. Any right recursion in such a + redirected notation is still interpreted as though it was really in + right associative level 200, i.e. the right recursion is at + level 200. Left recursive notations are not redirected. + + The redirection will be removed in the future and is therefore + deprecated. To keep the current behaviour, declare your notations at + level 10 and any recursion at level 200. For instance, + + .. rocqdoc:: + + Reserved Notation "'exists' x .. y , p" + (at level 200, x binder). + + becomes + + .. rocqdoc:: + + Reserved Notation "'exists' x .. y , p" + (at level 10, x binder, p at level 200). + + Finally note that any `associativity` annotation on notations + declared at level 200 are currrently ignored to avoid interfering + with the redirection to left-associative level 10 (`#21671 + `_, by Gaëtan + Gilbert). +- **Added:** + Print the location a notation was defined (and where it was reserved) when using `Locate` + (`#22194 `_, + by Johannes Hostert). + +Tactics +^^^^^^^ + +- **Changed:** + Stop zeta-normalizing generalized rewriting proofs for better + sharing and performance + (`#21631 `_, + by Matthieu Sozeau). +- **Changed:** + :tacn:`abstract`-ed subproofs within tactic quotations are not + inlined any more. The previous behavior can be restored through + the deprecated :flag:`Inline Abstract Subproof` flag + (`#21676 `_, + fixes `#7905 `_, + by Pierre-Marie Pédrot). +- **Changed:** + Generalize DeclareScheme to be able to register schemes for any GlobRef, + and not just for inductive types + (`#21811 `_, + by Thomas Lamiaux). +- **Changed:** + hints from a functor argument whose underlying reference is + marked Inline in the functor parameter type are not expanded + into their inlined value anymore at application time. This + prevents arbitrary terms from flowing into hint databases. + This change is not backwards compatible but breakage should + be extremely uncommon + (`#21862 `_, + by Pierre-Marie Pédrot). + + .. _93elim: + +- **Changed:** + Extend generation of eliminators to handle nesting with Primitive Arrays + (`#21928 `_, + by Léo Soudant). +- **Changed:** + :tacn:`clear` checks that identifiers are bound even when they are ltac variables + (typically in `match goal with H : _ |- _ => foo H; clear H end`, `clear` now fails if `foo` cleared H where before it would succeed without doing anything) + (`#21987 `_, + by Gaëtan Gilbert). +- **Changed:** + :tacn:`generalize_eqs_vars` (used in :tacn:`dependent induction`) + does less useless generalizations + (`#22001 `_, + fixes `#22000 `_, + by Gaëtan Gilbert). +- **Changed:** + The autorewrite tactic now accepts a direction: `autorewrite <- with xyz` + reverses the direction of rewriting rules registered in `xyz` (`#22184 + `_, fixes `#1875 + `_, by Clément Pit-Claudel). +- **Changed:** + `...` (:cmd:`Proof with`) is not deprecated anymore and is expected to remain available + (`#22251 `_, + by Gaëtan Gilbert). +- **Removed:** + the ability to use non-reference hints in `using` clauses + of :tacn:`auto`-like tactics + (`#21833 `_, + by Pierre-Marie Pédrot). +- **Added:** + Add :n:`matches` and :n:`tactic` :ref:`strategies ` + to :tacn:`rewrite_strat` for :ref:`Ltac1 ` and :ref:`Ltac2 ` tactics + (`#21521 `_, + by Matthieu Sozeau and Mathis Bouverot-Dupuis). +- **Fixed:** + Support primitive operations in old and new unification + (`#20175 `_, + fixes `#18259 `_ + and `#20155 `_, + by Jan-Oliver Kaiser). + + .. _93confusion: + +- **Fixed:** + the proof engine now keeps track of which hypotheses are section variables + instead of assuming that a variable sharing a name with a section variable is a section variable. + In particular :tacn:`destruct` now clears non-section-variable variables which share a name with a section variable. + Note that modifying a section variable (e.g. with `apply in`) makes it a non-section-variable + (`#21987 `_, + fixes `#18858 `_ + and `#12304 `_ + and `#11487 `_ + and `#6773 `_, + by Gaëtan Gilbert). +- **Fixed:** + Fix generation of eliminators for not recursive inductive types but with non-uniform parameters + (`#22154 `_, + fixes `#22149 `_, + by Thomas Lamiaux). +- **Fixed:** + :tacn:`clear` does not unshelve previously shelved evars + (`#22182 `_, + fixes `#22076 `_ + and `#21831 `_, + by Gaëtan Gilbert). + +Ltac2 language +^^^^^^^^^^^^^^ + +- **Changed:** + Parse ``match`` expressions at level 0 instead of level 5 + (`#22092 `_, + by Rodolphe Lepigre). +- **Added:** + scopes for :cmd:`Ltac2 Notation` to pick the interpretation at (Ltac2) typechecking time instead of parsing time, + similar to term notation scopes + (`#21542 `_, + fixes `#16538 `_ + and `#17330 `_, + by Gaëtan Gilbert). +- **Added:** + Low-level operations to manipulate transparent states: + 1. Set-like operations (union, intersection, difference). + 2. Operations to add/remove/test membership of constants, variables, and primitive projections. + (`#21558 `_, + by Mathis Bouverot-Dupuis). +- **Added:** + :cmd:`Ltac2 Abbreviation` typecheck the body at declaration time instead of when they are used. + This means incorrect abbreviations produce errors at declaration time, and also means quotations may be used inside abbreviations + (e.g. `Ltac2 Abbreviation foo := @foo.`) + (`#21617 `_, + by Gaëtan Gilbert). +- **Added:** + `Ltac2.Control.reorder_goals` + (`#21642 `_, + fixes `#20087 `_, + by Gaëtan Gilbert). +- **Added:** + ``Scheme.lookup`` in Ltac2 to look up registered inductive schemes + (elimination, case analysis, etc.) by scheme kind (`#21658 + `_, fixes `#20987 + `_, by Jason Gross). +- **Added:** + :tacn:`with_strategy` to Ltac2, to allow temporarily changing the strategy + level of constants during tactic execution, with automatic restoration + afterward + (`#21762 `_, + by Jason Gross). + + .. _93ltac2not: + +- **Added:** + Add OCaml-inspired `@@` and `|>` notations + (`#21819 `_, + by Jan-Oliver Kaiser). +- **Added:** + ``Scheme.scase_dep`` and ``Scheme.scase_nodep`` in Ltac2 for SProp case + analysis scheme kinds, and support for registering SProp case schemes via the + :cmd:`Scheme` command + (`#21881 `_, + by Jason Gross). + +SSReflect +^^^^^^^^^ + +.. _93ssrrw: + +- **Changed:** + ``rewrite`` tactic for ``rw``. Since this was the major cause of + conflict with legacy tactics, ssreflect can now be loaded with less + conflicts through ``From Corelib Require Import ssreflect_rw.``. + For backward compatibility + ``From Corelib Require Import ssreflect.`` + still loads a ``rewrite`` wrapper to ``rw`` as well as the + ``if is then else `` + and ``if isn't then else `` + syntactic sugars for match + (`#21478 `_, + by Pierre Roux). +- **Removed:** + the `of T` syntax for anonymous binders outside of constructors, + use `& T` instead + (`#21611 `_, + by Pierre Roux). +- **Fixed:** + Handling of universe polymorphism by ssrmatching (e.g. :tacn:`unlock` and :tacn:`rw` tactics), + now recording appropriate universe unifications. + (`#22096 `_, + fixes `#22086 `_, + by Matthieu Sozeau). +- **Fixed:** + Ssreflect generalization through views in presence of universe polymorphism + (`#22169 `_, + fixes `#22158 `_, + by Matthieu Sozeau). + +Commands and options +^^^^^^^^^^^^^^^^^^^^ + +- **Changed:** + Generalize :cmd:`About` to be able to handle several definitions at once + (`#21823 `_, + by Thomas Lamiaux). +- **Changed:** + the behavior of the :flag:`Asymmetric Patterns` flag, which no + longer disactivates implicit arguments in patterns. Set the + compatibility flag :flag:`Asymmetric Patterns No Implicits` to + retrieve the previous behavior + (`#21947 `_, + fixes `#21769 `_, + by Pierre Roux). +- **Changed:** + Generalize :cmd:`Print` command to print multiples definitions + (`#22017 `_, + by Elsa Rabu). +- **Changed:** + `rocq dep` errors have more readable locations, and warnings have locations + (`#22231 `_, + fixes `#10815 `_, + by Gaëtan Gilbert). +- **Removed:** + `-verbose` and `load-vernac-source-verbose` (`-lv`). + `-verbose` has been ignored for several versions. + `-lv` would print the input file (as-is from source, not pretty printed) + which does not seem useful + (`#21626 `_, + by Gaëtan Gilbert). + + .. _93alloclimit: + +- **Added:** + :cmd:`AllocLimit` and :tacn:`alloc_limit` to enforce allocation limits during execution + (`#17266 `_, + by Gaëtan Gilbert). +- **Added:** + approximate matching in :cmd:`Search`, controlled by new option :opt:`Fuzzy Search`. + Currently only when searching by name (:n:`Search @string`) + (`#20660 `_, + by Gaëtan Gilbert). +- **Added:** + flag :flag:`Printing Regular Matches` to disable alternate match syntaxes + (`#21645 `_, + by Gaëtan Gilbert). +- **Added:** + flag :flag:`Indices Matter` to set ``-indices-matter`` locally, + controlling whether the types of indices of inductive types + contribute universe constraints + (`#21779 `_, + by Jason Gross). +- **Added:** + warning when an interactive proof is not started by :cmd:`Proof`, and error when :cmd:`Proof` is used multiple times or is used after a tactic has been used + (`#21865 `_, + by Gaëtan Gilbert). +- **Added:** + a `Print Debug Delta` vernacular command to print debug + information about module delta-resolvers + (`#21867 `_, + by Pierre-Marie Pédrot). +- **Added:** + :cmd:`Print Grammar` with argument `Tree` to print the factorizations done by the grammar engine + (`#21934 `_, + by Gaëtan Gilbert). +- **Added:** + :flag:`Proof Using Clear Unused` which automatically clears variables not allowed by a :cmd:`Proof using` annotation at the beginning of an interactive proof + (`#22107 `_, + by Gaëtan Gilbert). +- **Added:** + The :table:`Search Blacklist` table now accepts plain references, that + are excluded from the Search results + (`#22193 `_, + by Pierre-Marie Pédrot). +- **Fixed:** fallback printing of inductives using + ```` now prints correctly + (though with possibly more qualification than needed) + (it should in any case only happen rarely from module errors) + (`#21484 `_, by Gaëtan Gilbert). +- **Fixed:** The default name of the induction principle in :g:`SProp` + generated by :g:`Scheme Induction for T Sort SProp` is now correct. It is now + :g:`T_sind`, instead of :g:`T_inds`. Similarly for :g:`Case`, the name will + now be :g:`T_scase` instead of :g:`T_cases`. + (`#21578 `_, + by Jean Caspar). +- **Fixed:** + :cmd:`Print Assumptions` now also traverses the types of global + definitions, not just their bodies, to detect dependencies on axioms + that appear only in the type + (`#21825 `_, + by Jason Gross). + +Command-line tools +^^^^^^^^^^^^^^^^^^ + +.. _93alectryon: + +- **Added:** + New Alectryon Markdown backend for `rocq doc` + (`#21950 `_, + by Dario Halilovic). +- **Fixed:** + ``rocq wc`` now handles tactics containing the word ``Proof`` correctly. + (`#21423 `_, + fixes `#21422 `_, + by Johannes Hostert). + +Corelib +^^^^^^^ + +- **Changed:** number notations for `nat` `Number.int` and `Number.uint` are + now declared in `NumberNotations` submodules of `Nat` and `Number`. The + submodules are exported from `Nat` and `Number` (which are not imported by + default) and from `Prelude` (which is imported by default) so visible changes + should be rare (`#21971 `_, by + Gaëtan Gilbert). +- **Fixed:** + Rewriting schemes over template polymorphic inductive types + (generated by :cmd:`Scheme` ``Rewriting``, or on the fly by tactics + such as :tacn:`rewrite` on user-defined equality types) no longer + mention the global template universes in their types. In + particular, the types of ``eq_sym``, ``eq_sym_involutive`` and + ``eq_rew_r_dep`` now use a universe local to the scheme instead of + ``eq.u0``, so that using these constants no longer adds constraints + on ``eq.u0`` (which is deprecated, see the ``bad-template-constraint`` + warning) + (`#22221 `_, + fixes `#22220 `_, + by Jason Gross). + +Infrastructure and dependencies +^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ + +.. _93dune321: + +- **Changed:** + Require ``dune`` version 3.21.0 to support the ``rocq.theory`` stanza + (`#21660 `_, + by Rodolphe Lepigre). + + .. _93package: + +- **Added:** + New notion of Rocq package and installation layout supported by a new + command-line option ``-package DEP`` that automatically adds the correct + ``-Q`` and ``-I`` options for ``DEP`` and its transitive dependencies. + For backwards compatibility, the old installation scheme targeting the + ``coq/user-contrib`` directory is kept, but the plan is to remove it + after packages have been ported to the new installation scheme. + The ``rocq makefile`` command can be made to rely on the new installation + scheme by passing the ``--rocq-package PKGNAME`` argument, and optionally + the ``--legacy-support`` argument to also install using the legacy + installation scheme + (`#21564 `_, + by Rodolphe Lepigre). +- **Fixed:** + building Rocq on Windows with Dune 3.24 or later + (path normalization in custom Rocq rules went awry) + (`#22198 `_, + by Gaëtan Gilbert). + +Miscellaneous +^^^^^^^^^^^^^ + +- **Removed:** + legacy loading mode for plugins, that was deprecated in Rocq 9.0. + To adapt, change your ``Declare ML Module "legacy:current".`` + to ``Declare ML Module "current".`` + (`#21852 `_, + by Pierre Roux). +- **Fixed:** + ``EConstr.contract_case`` no longer anomalies when Case branches + contain evar-backed Lambda bodies (e.g., from ``Constr.in_context``) + (`#22058 `_, + by Jason Gross). + + Version 9.2 ----------- diff --git a/doc/sphinx/language/extensions/match.rst b/doc/sphinx/language/extensions/match.rst index da50a14435c5..e68723b52f40 100644 --- a/doc/sphinx/language/extensions/match.rst +++ b/doc/sphinx/language/extensions/match.rst @@ -66,6 +66,8 @@ can be alternatively written Definition not (b:bool) := if b then false else true. +See also :ref:`SSReflect documentation ` for more examples. + .. deprecated:: 9.3 More generally, for an inductive type with constructors :n:`@ident__1`