rocq-prover · coqbot-app · Jul 20, 2026 · Jul 15, 2026
@@ -37,6 +37,7 @@ Martin Bodin <martin.bodin@ens-lyon.org>           Martin Bodin <mbodin@ic.ac.uk
 Martin Bodin <martin.bodin@ens-lyon.org>           Martin Bodin <martin.bodin@inria.fr>
 Mathis Bouverot <mathis.bouverot@ens.psl.eu>       MathisBD <mathis.bouverot@ens.psl.eu> 
 Ana Borges <ana.agvb@gmail.com>                    Ana <ana.agvb@gmail.com>
+Peio Borthelle <peio.borthelle@inria.fr>           Lapin0t
 @drenched-moth < >                                   drenched-moth <85354652+drenched-moth@users.noreply.github.com>
 Ana Borges <ana.agvb@gmail.com>                    ana-borges <ana-borges@users.noreply.github.com>
 Felix Loyau-Kahn <felix.loyau-kahn@etu.u-paris.fr>         felixL-K <felix.loyau-kahn@etu.u-paris.fr>
@@ -47,6 +48,7 @@ Pierre Boutillier <pierre.boutillier@ens-lyon.org> Pierre <pierre.boutillier@ens
 Pierre Boutillier <pierre.boutillier@ens-lyon.org> Pierre Boutillier <pierre.boutillier@pps.univ-paris-diderot.fr>
 Michele Caci <michele.caci@gmail.com>              mcaci <michele.caci@gmail.com>
 Ali Caglayan <alizter@gmail.com>                   Alizter <Alizter@users.noreply.github.com>
+Matteo Calosci <calosci.matteo98@gmail.com>        CalosciMatteo <calosci.matteo98@gmail.com>
 Arthur Charguéraud <arthur@chargueraud.org>        charguer <arthur@chargueraud.org>
 chluebi <42419603+chluebi@users.noreply.github.com>  chluebi <42419603+chluebi@users.noreply.github.com>
 Tej Chajed <tchajed@mit.edu>                       tchajed
@@ -253,6 +255,7 @@ Enrico Tassi <Enrico.Tassi@inria.fr>               gares <gares@users.noreply.gi
 Enrico Tassi <Enrico.Tassi@inria.fr>               gares <gares@fettunta.org>
 Romain Tetley <romain.tetley@inria.fr>             rtetley
 Guillaume Munch-Maccagnoni <guillaume.munch-maccagnoni@inria.fr>  gadmm
+Dario Halilovic                                    dhalilov
 Hendrik Tews <Hendrik.Tews@kernkonzept.com>        Hendrik Tews <tews@elite.askra.de>
 Laurent Théry <laurent.thery@inria.fr>             thery <thery@85f007b7-540e-0410-9357-904b9bb8a0f7>
 Laurent Théry <laurent.thery@inria.fr>             thery <thery@sophia.inria.fr>

diff --git a/doc/changelog/01-kernel/21416-record-postponed-eta-Changed.rst b/doc/changelog/01-kernel/21416-record-postponed-eta-Changed.rst
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
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
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
diff --git a/doc/changelog/01-kernel/21774-track-indices-matter-Added.rst b/doc/changelog/01-kernel/21774-track-indices-matter-Added.rst
diff --git a/doc/changelog/01-kernel/21845-guard-fix-subterm-Fixed.rst b/doc/changelog/01-kernel/21845-guard-fix-subterm-Fixed.rst
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
diff --git a/doc/changelog/01-kernel/22058-einductive-contract-case-Fixed.rst b/doc/changelog/01-kernel/22058-einductive-contract-case-Fixed.rst
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
diff --git a/doc/changelog/02-specification-language/21450-elab-sorts-Added.rst b/doc/changelog/02-specification-language/21450-elab-sorts-Added.rst
diff --git a/doc/changelog/02-specification-language/21611-if-is.rst b/doc/changelog/02-specification-language/21611-if-is.rst
diff --git a/doc/changelog/02-specification-language/21611-of-ampersand.rst b/doc/changelog/02-specification-language/21611-of-ampersand.rst
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
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
diff --git a/doc/changelog/02-specification-language/22123-deprecate-if-Deprecated.rst b/doc/changelog/02-specification-language/22123-deprecate-if-Deprecated.rst
diff --git a/doc/changelog/02-specification-language/22124-if-printing-Removed.rst b/doc/changelog/02-specification-language/22124-if-printing-Removed.rst
diff --git a/doc/changelog/02-specification-language/22170-belowtype-Fixed.rst b/doc/changelog/02-specification-language/22170-belowtype-Fixed.rst
diff --git a/doc/changelog/02-specification-language/22207-record-with-Added.rst b/doc/changelog/02-specification-language/22207-record-with-Added.rst
diff --git a/doc/changelog/03-notations/21671-binder-constr-Changed.rst b/doc/changelog/03-notations/21671-binder-constr-Changed.rst
diff --git a/doc/changelog/03-notations/22194-master-Added.rst b/doc/changelog/03-notations/22194-master-Added.rst
diff --git a/doc/changelog/04-tactics/20175-janno-unif-red-prim.rst b/doc/changelog/04-tactics/20175-janno-unif-red-prim.rst
diff --git a/doc/changelog/04-tactics/21521-strat-pattern-ltac-Added.rst b/doc/changelog/04-tactics/21521-strat-pattern-ltac-Added.rst
diff --git a/doc/changelog/04-tactics/21631-stop-zeta-rewrite-Changed.rst b/doc/changelog/04-tactics/21631-stop-zeta-rewrite-Changed.rst
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
diff --git a/doc/changelog/04-tactics/21811-genScheme-Changed.rst b/doc/changelog/04-tactics/21811-genScheme-Changed.rst
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
diff --git a/doc/changelog/04-tactics/21862-cleanup-hints-globref-Changed.rst b/doc/changelog/04-tactics/21862-cleanup-hints-globref-Changed.rst
diff --git a/doc/changelog/04-tactics/21928-arrayall-Changed.rst b/doc/changelog/04-tactics/21928-arrayall-Changed.rst
diff --git a/doc/changelog/04-tactics/21987-context-secvar-Changed.rst b/doc/changelog/04-tactics/21987-context-secvar-Changed.rst
diff --git a/doc/changelog/04-tactics/21987-context-secvar-Fixed.rst b/doc/changelog/04-tactics/21987-context-secvar-Fixed.rst
diff --git a/doc/changelog/04-tactics/22001-gene-eqs-vars-Changed.rst b/doc/changelog/04-tactics/22001-gene-eqs-vars-Changed.rst
diff --git a/doc/changelog/04-tactics/22154-fix-rec-Fixed.rst b/doc/changelog/04-tactics/22154-fix-rec-Fixed.rst
diff --git a/doc/changelog/04-tactics/22182-clear-shelf-Fixed.rst b/doc/changelog/04-tactics/22182-clear-shelf-Fixed.rst
diff --git a/doc/changelog/04-tactics/22184-master-Changed.rst b/doc/changelog/04-tactics/22184-master-Changed.rst
diff --git a/doc/changelog/04-tactics/22251-underp-proof-with-Changed.rst b/doc/changelog/04-tactics/22251-underp-proof-with-Changed.rst
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
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
diff --git a/doc/changelog/06-Ltac2-language/21617-tac2abbrev-up-Added.rst b/doc/changelog/06-Ltac2-language/21617-tac2abbrev-up-Added.rst
diff --git a/doc/changelog/06-Ltac2-language/21642-redoer-goals-Added.rst b/doc/changelog/06-Ltac2-language/21642-redoer-goals-Added.rst
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
diff --git a/doc/changelog/06-Ltac2-language/21762-ltac2-strategy-Added.rst b/doc/changelog/06-Ltac2-language/21762-ltac2-strategy-Added.rst
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
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
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
diff --git a/doc/changelog/07-ssreflect/21478-ssreflect-rw-Changed.rst b/doc/changelog/07-ssreflect/21478-ssreflect-rw-Changed.rst
diff --git a/doc/changelog/07-ssreflect/21611-of-ampersand-of-Removed.rst b/doc/changelog/07-ssreflect/21611-of-ampersand-of-Removed.rst
diff --git a/doc/changelog/07-ssreflect/22096-fix-ssr-univpoly-Fixed.rst b/doc/changelog/07-ssreflect/22096-fix-ssr-univpoly-Fixed.rst
diff --git a/doc/changelog/07-ssreflect/22169-fix-22158-Fixed.rst b/doc/changelog/07-ssreflect/22169-fix-22158-Fixed.rst
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
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
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