From 1a8c2ce4b1c26975ebf4e182c75bea26ce6efa28 Mon Sep 17 00:00:00 2001
From: Enrico Tassi <Enrico.Tassi@Inria.fr>
Date: Wed, 8 Jul 2026 22:52:44 +0200
Subject: [PATCH 01/28] doc for 9.3

(cherry picked from commit 65769ad687259d3c8d17e53959d39668e0741a4f)
---
 doc/sphinx/conf.py | 1 +
 1 file changed, 1 insertion(+)

diff --git a/doc/sphinx/conf.py b/doc/sphinx/conf.py
index 2d32b1cde61a..06c287b23c45 100644
--- a/doc/sphinx/conf.py
+++ b/doc/sphinx/conf.py
@@ -211,6 +211,7 @@ def setup(app):
     'versions': [
         ("dev", "https://rocq-prover.org/doc/master/refman/"),
         ("stable", "https://rocq-prover.org/refman/"),
+        ("9.3", "https://rocq-prover.org/doc/v9.3/refman/"),
         ("9.2", "https://rocq-prover.org/doc/v9.2/refman/"),
         ("9.1", "https://rocq-prover.org/doc/v9.1/refman/"),
         ("9.0", "https://rocq-prover.org/doc/v9.0/refman/"),

From 7c616cfddf4acda4759ec6a1f0033da31f30e5af Mon Sep 17 00:00:00 2001
From: Enrico Tassi <Enrico.Tassi@Inria.fr>
Date: Wed, 8 Jul 2026 22:53:06 +0200
Subject: [PATCH 02/28] update doc to tags for 9.0, 9.1 and 9.2

(cherry picked from commit a9434da7bc923a96d4d6329b9a55d19fe6645000)
---
 doc/sphinx/conf.py | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/doc/sphinx/conf.py b/doc/sphinx/conf.py
index 06c287b23c45..2c20e1860093 100644
--- a/doc/sphinx/conf.py
+++ b/doc/sphinx/conf.py
@@ -212,9 +212,9 @@ def setup(app):
         ("dev", "https://rocq-prover.org/doc/master/refman/"),
         ("stable", "https://rocq-prover.org/refman/"),
         ("9.3", "https://rocq-prover.org/doc/v9.3/refman/"),
-        ("9.2", "https://rocq-prover.org/doc/v9.2/refman/"),
-        ("9.1", "https://rocq-prover.org/doc/v9.1/refman/"),
-        ("9.0", "https://rocq-prover.org/doc/v9.0/refman/"),
+        ("9.2", "https://rocq-prover.org/doc/V9.2.0/refman/"),
+        ("9.1", "https://rocq-prover.org/doc/V9.1.1/refman/"),
+        ("9.0", "https://rocq-prover.org/doc/V9.0.1/refman/"),
         ("8.20", "https://rocq-prover.org/doc/V8.20.1/refman/"),
         ("8.19", "https://rocq-prover.org/doc/V8.19.2/refman/"),
         ("8.18", "https://rocq-prover.org/doc/V8.18.0/refman/"),

From 30d810b5ec41902b9e44e6c6eada495c226297a6 Mon Sep 17 00:00:00 2001
From: Pierre Roux <pierre.roux@onera.fr>
Date: Thu, 9 Jul 2026 09:32:09 +0200
Subject: [PATCH 03/28] [rocq makefile] Don't erase ROCQPATH

Fixing an unfortunate variable overlap from
https://github.com/rocq-prover/rocq/pull/21564

(cherry picked from commit e964f5c5025093b949298fa1510f5e4c33368b53)
---
 tools/CoqMakefile.in  | 10 +++++-----
 tools/rocqmakefile.ml |  4 ++--
 2 files changed, 7 insertions(+), 7 deletions(-)

diff --git a/tools/CoqMakefile.in b/tools/CoqMakefile.in
index 200c09a5d1c3..87b5fb59418d 100644
--- a/tools/CoqMakefile.in
+++ b/tools/CoqMakefile.in
@@ -29,8 +29,8 @@ MLLIBFILES        := $(COQMF_MLLIBFILES)
 METAFILE          := $(COQMF_METAFILE)
 ROCQPACKAGE       := $(COQMF_ROCQPACKAGE)
 LEGACYSUPPORT     := $(COQMF_LEGACY_SUPPORT)
-HASROCQPATH       := $(COQMF_HAS_ROCQPATH)
-ROCQPATH          := $(COQMF_ROCQPATH)
+HAS_PACKAGE_LOGICAL_PATH := $(COQMF_HAS_PACKAGE_LOGICAL_PATH)
+PACKAGE_LOGICAL_PATH   := $(COQMF_PACKAGE_LOGICAL_PATH)
 CMDLINE_VFILES    := $(COQMF_CMDLINE_VFILES)
 INSTALLCOQDOCROOT := $(COQMF_INSTALLCOQDOCROOT)
 OTHERFLAGS        := $(COQMF_OTHERFLAGS)
@@ -596,8 +596,8 @@ install: META
 	$(call findlib_remove)
 	$(call findlib_install, META $(FINDLIBFILESTOINSTALL))
 	$(HIDE)if [ "$(ROCQPACKAGE)" ]; then \
-	 if [ "$(HASROCQPATH)" != "true" ]; then echo "Error: $(METAFILE) has no top-level rocqpath field"; exit 1; fi; \
-	 root="$(subst .,/,$(ROCQPATH))"; \
+	 if [ "$(HAS_PACKAGE_LOGICAL_PATH)" != "true" ]; then echo "Error: $(METAFILE) has no top-level rocqpath field"; exit 1; fi; \
+	 root="$(subst .,/,$(PACKAGE_LOGICAL_PATH))"; \
 	 for f in $$(cat .filestoinstall); do\
 	   df="`$(COQMKFILE) -destination-of "$$f" $(COQLIBS)`"; rc="$$?";\
 	   if [ "$$rc" != "0" -o -z "$$df" ]; then\
@@ -609,7 +609,7 @@ install: META
 	       case "$$df" in \
 	         "$$root") rel="" ;; \
 	         "$$root"/*) rel="$${df#$$root/}" ;; \
-	         *) echo SKIP "$$f" since it is outside rocqpath "$(ROCQPATH)"; continue ;; \
+	         *) echo SKIP "$$f" since it is outside rocqpath "$(PACKAGE_LOGICAL_PATH)"; continue ;; \
 	       esac; \
 	     else \
 	       case "$$rel" in /*) rel="$${rel#/}" ;; esac; \
diff --git a/tools/rocqmakefile.ml b/tools/rocqmakefile.ml
index 3acda768d96d..c943d773e357 100644
--- a/tools/rocqmakefile.ml
+++ b/tools/rocqmakefile.ml
@@ -435,8 +435,8 @@ let generate_conf_files oc p =
     | Some _, Present x -> read_meta_rocqpath x
     | _ -> None
   in
-  fprintf oc "COQMF_HAS_ROCQPATH = %s\n" (if Option.has_some rocqpath then "true" else "false");
-  fprintf oc "COQMF_ROCQPATH = %s\n" (Option.default "" rocqpath)
+  fprintf oc "COQMF_HAS_PACKAGE_LOGICAL_PATH = %s\n" (if Option.has_some rocqpath then "true" else "false");
+  fprintf oc "COQMF_PACKAGE_LOGICAL_PATH = %s\n" (Option.default "" rocqpath)
 
 let rec all_start_with prefix = function
   | [] -> true

From 2c9c88f702d3db2ec20fd8de1486c958804813af Mon Sep 17 00:00:00 2001
From: shilangyu <xmarcinmarcin@gmail.com>
Date: Sat, 25 Apr 2026 22:02:52 +0200
Subject: [PATCH 04/28] doc: store subdomain data in a class

This makes it easier to track what values we store for each object kind.

(cherry picked from commit 9f730cc8a223f8a708d9a28c8793938311ddd877)
---
 doc/tools/rocqrst/rocqdomain.py | 43 +++++++++++++++++++--------------
 1 file changed, 25 insertions(+), 18 deletions(-)

diff --git a/doc/tools/rocqrst/rocqdomain.py b/doc/tools/rocqrst/rocqdomain.py
index 65051ffcce90..dc706e3d5642 100644
--- a/doc/tools/rocqrst/rocqdomain.py
+++ b/doc/tools/rocqrst/rocqdomain.py
@@ -24,6 +24,7 @@
 import re
 import shlex
 from itertools import chain
+from dataclasses import dataclass
 from collections import defaultdict
 
 from docutils import nodes, utils
@@ -84,6 +85,13 @@ def visit_desc_signature(self, node):
 Offending notation: {}
 Error message: {}"""
 
+@dataclass
+class SubdomainItemData:
+    """Data stored for each object in a subdomain"""
+    docname: str
+    objtype: str
+    targetid: str
+
 def notation_to_sphinx(notation, source, line, rawtext=None):
     """Parse notation and wrap it in an inline node"""
     try:
@@ -179,7 +187,7 @@ def _render_signature(self, signature, signode):
         'noindex': directives.flag
     }
 
-    def subdomain_data(self):
+    def subdomain_data(self) -> dict[str, SubdomainItemData]:
         if self.subdomain is None:
             raise ValueError()
         return self.env.domaindata['rocq']['objects'][self.subdomain]
@@ -207,11 +215,11 @@ def handle_signature(self, signature, signode):
             names = [name] if name else None
         return names
 
-    def _warn_if_duplicate_name(self, objects, name, signode):
+    def _warn_if_duplicate_name(self, objects: dict[str, SubdomainItemData], name: str, signode):
         """Check that two objects in the same domain don't have the same name."""
         if name in objects:
             MSG = 'Duplicate name {} (other is in {}) attached to {}'
-            msg = MSG.format(name, self.env.doc2path(objects[name][0]), signode)
+            msg = MSG.format(name, self.env.doc2path(objects[name].docname), signode)
             self.state_machine.reporter.warning(msg, line=self.lineno)
 
     def _record_name(self, name, target_id, signode):
@@ -222,7 +230,7 @@ def _record_name(self, name, target_id, signode):
         """
         names_in_subdomain = self.subdomain_data()
         self._warn_if_duplicate_name(names_in_subdomain, name, signode)
-        names_in_subdomain[name] = (self.env.docname, self.objtype, target_id)
+        names_in_subdomain[name] = SubdomainItemData(self.env.docname, self.objtype, target_id)
 
     def _target_id(self, name):
         return make_target(self.objtype, make_id(name))
@@ -975,12 +983,12 @@ def generate(self, docnames=None):
         items = chain(*(self.domain.data['objects'][subdomain].items()
                         for subdomain in self.subdomains))
 
-        for itemname, (docname, _, anchor) in sorted(items, key=lambda x: x[0].lower()):
-            if docnames and docname not in docnames:
+        for itemname, data in sorted(items, key=lambda x: x[0].lower()):
+            if docnames and data.docname not in docnames:
                 continue
 
             entries = content[itemname[0].lower()]
-            entries.append([itemname, 0, docname, anchor, '', '', ''])
+            entries.append([itemname, 0, data.docname, data.targetid, '', '', ''])
 
         collapse = False
         content = sorted(content.items())
@@ -1158,7 +1166,7 @@ class RocqDomain(Domain):
     initial_data = {
         # Collect everything under a key that we control, since Sphinx adds
         # others, such as “version”
-        'objects' : { # subdomain → name → docname, objtype, targetid
+        'objects' : { # subdomain → name → SubdomainItemData
             'cmd': {},
             'tacn': {},
             'opt': {},
@@ -1182,8 +1190,8 @@ def find_index_by_name(targetid):
     def get_objects(self):
         # Used for searching and object inventories (intersphinx)
         for _, objects in self.data['objects'].items():
-            for name, (docname, objtype, targetid) in objects.items():
-                yield (name, name, objtype, docname, targetid, self.object_types[objtype].attrs['searchprio'])
+            for name, data in objects.items():
+                yield (name, name, data.objtype, data.docname, data.targetid, self.object_types[data.objtype].attrs['searchprio'])
         for index in self.indices:
             yield (index.name, index.localname, 'index', "rocq-" + index.name, '', -1)
 
@@ -1191,11 +1199,11 @@ def merge_domaindata(self, docnames, otherdata):
         DUP = "Duplicate declaration: '{}' also defined in '{}'.\n"
         for subdomain, their_objects in otherdata['objects'].items():
             our_objects = self.data['objects'][subdomain]
-            for name, (docname, objtype, targetid) in their_objects.items():
-                if docname in docnames:
+            for name, data in their_objects.items():
+                if data.docname in docnames:
                     if name in our_objects:
-                        self.env.warn(docname, DUP.format(name, our_objects[name][0]))
-                    our_objects[name] = (docname, objtype, targetid)
+                        self.env.warn(data.docname, DUP.format(name, our_objects[name].docname))
+                    our_objects[name] = data
 
     def resolve_xref(self, env, fromdocname, builder, role, targetname, node, contnode):
         # ‘target’ is the name that was written in the document
@@ -1207,14 +1215,13 @@ def resolve_xref(self, env, fromdocname, builder, role, targetname, node, contno
         else:
             resolved = self.data['objects'][role].get(targetname)
             if resolved:
-                (todocname, _, targetid) = resolved
-                return make_refnode(builder, fromdocname, todocname, targetid, contnode, targetname)
+                return make_refnode(builder, fromdocname, resolved.docname, resolved.targetid, contnode, targetname)
         return None
 
     def clear_doc(self, docname_to_clear):
         for subdomain_objects in self.data['objects'].values():
-            for name, (docname, _, _) in list(subdomain_objects.items()):
-                if docname == docname_to_clear:
+            for name, data in list(subdomain_objects.items()):
+                if data.docname == docname_to_clear:
                     del subdomain_objects[name]
 
 def is_rocqtop_or_rocqdoc_block(node):

From b4c22209385a963804ed8d93298c8406a1b5aa00 Mon Sep 17 00:00:00 2001
From: shilangyu <xmarcinmarcin@gmail.com>
Date: Sun, 26 Apr 2026 16:44:36 +0200
Subject: [PATCH 05/28] doc: serialize syntax for subdomain data

(cherry picked from commit 4a7a65386ff5b2c2a2066273702ccd6d699a45f6)
---
 doc/tools/rocqrst/notations/object.py | 111 ++++++++++++++++++++++++++
 doc/tools/rocqrst/rocqdomain.py       |  27 +++++--
 2 files changed, 131 insertions(+), 7 deletions(-)
 create mode 100644 doc/tools/rocqrst/notations/object.py

diff --git a/doc/tools/rocqrst/notations/object.py b/doc/tools/rocqrst/notations/object.py
new file mode 100644
index 000000000000..ce9b8f644426
--- /dev/null
+++ b/doc/tools/rocqrst/notations/object.py
@@ -0,0 +1,111 @@
+from dataclasses import asdict, dataclass
+
+from .parsing import parse
+from .TacticNotationsParser import TacticNotationsParser
+from .TacticNotationsVisitor import TacticNotationsVisitor
+
+
+class NotationObject:
+    def asdict(self):
+        return asdict(self)
+
+@dataclass
+class Literal(NotationObject):
+    value: str
+    subscript: str | None
+    type = "literal"
+
+@dataclass
+class Reference(NotationObject):
+    value: str
+    subscript: str | None
+    type = "reference"
+
+@dataclass
+class Alternative(NotationObject):
+    children: list[NotationObject]
+    type = "alternative"
+
+@dataclass
+class Repeat(NotationObject):
+    min: int
+    max: int | None
+    separator: str | None
+    children: list[NotationObject]
+    type = "repeat"
+
+class TacticNotationsToObjectVisitor(TacticNotationsVisitor):
+    def defaultResult(self):
+        return []
+
+    def aggregateResult(self, aggregate, nextResult):
+        # Flattening results into a single list of nodes
+        if nextResult:
+            if isinstance(nextResult, list):
+                aggregate.extend(nextResult)
+            else:
+                aggregate.append(nextResult)
+        return aggregate
+
+    def visitAlternative(self, ctx: TacticNotationsParser.AlternativeContext):
+        return [Alternative(children=self.visitChildren(ctx))]
+
+    def visitAltblock(self, ctx: TacticNotationsParser.AltblockContext):
+        return self.visitChildren(ctx)
+
+    def visitRepeat(self, ctx: TacticNotationsParser.RepeatContext):
+        separator = ctx.ATOM() or ctx.PIPE()
+        # skip the '{'
+        repeat_marker = ctx.LGROUP().getText()[1]
+
+        min_rep, max_rep = None, None
+        match repeat_marker:
+            case "?":
+                min_rep, max_rep = 0, 1
+            case "+":
+                min_rep, max_rep = 1, None
+            case "*":
+                min_rep, max_rep = 0, None
+            case _:
+                raise ValueError(f"Unexpected repeat marker: {repeat_marker}")
+
+        return [Repeat(
+            min=min_rep,
+            max=max_rep,
+            separator=separator.getText() if separator else None,
+            children=self.visitChildren(ctx)
+        )]
+
+    def visitCurlies(self, ctx: TacticNotationsParser.CurliesContext):
+        return [
+            Literal(value=ctx.LBRACE().getText(), subscript=None),
+            *self.visitChildren(ctx),
+            Literal(value=ctx.RBRACE().getText(), subscript=None)]
+
+    def visitAtomic(self, ctx: TacticNotationsParser.AtomicContext):
+        return [Literal(
+            value=ctx.ATOM().getText(),
+            # skip '__'
+            subscript=ctx.SUB().getText()[2:] if ctx.SUB() else None
+        )]
+
+    def visitHole(self, ctx: TacticNotationsParser.HoleContext):
+        return [Reference(
+            value=ctx.ID().getText()[1:],
+            # skip '__'
+            subscript=ctx.SUB().getText()[2:] if ctx.SUB() else None
+        )]
+
+    def visitEscaped(self, ctx: TacticNotationsParser.EscapedContext):
+        return [Literal(
+            value=ctx.ESCAPED().getText().replace("%", ""),
+            subscript=None
+        )]
+
+def objectify(notation: str) -> list[NotationObject]:
+    """Translate a notation into an object.
+
+    It is essentially a simplified and normalized version of the ANTLR AST.
+    """
+    visitor = TacticNotationsToObjectVisitor()
+    return visitor.visit(parse(notation))
diff --git a/doc/tools/rocqrst/rocqdomain.py b/doc/tools/rocqrst/rocqdomain.py
index dc706e3d5642..f7ed75f047c5 100644
--- a/doc/tools/rocqrst/rocqdomain.py
+++ b/doc/tools/rocqrst/rocqdomain.py
@@ -48,6 +48,7 @@
 from .repl.rocqtop import RocqTop, RocqTopError
 from .notations.parsing import ParseError
 from .notations.sphinx import sphinxify
+from .notations import object as object_notations
 from .notations.plain import stringify_with_ellipses
 
 # FIXME: Patch this in Sphinx
@@ -91,6 +92,7 @@ class SubdomainItemData:
     docname: str
     objtype: str
     targetid: str
+    syntax: list[object_notations.NotationObject]
 
 def notation_to_sphinx(notation, source, line, rawtext=None):
     """Parse notation and wrap it in an inline node"""
@@ -178,6 +180,14 @@ def _render_signature(self, signature, signode):
         """Render a signature, placing resulting nodes into signode."""
         raise NotImplementedError(self)
 
+    def _signature_to_syntax(self, signature: str) -> list[object_notations.NotationObject]:
+        """Convert a signature into a syntax tree, used in generated plain JSON indices.
+
+        By default, returns the signature as a literal string.
+
+        """
+        return [object_notations.Literal(value=signature, subscript=None)]
+
     option_spec = {
         # Explicit object naming
         'name': directives.unchanged,
@@ -222,7 +232,7 @@ def _warn_if_duplicate_name(self, objects: dict[str, SubdomainItemData], name: s
             msg = MSG.format(name, self.env.doc2path(objects[name].docname), signode)
             self.state_machine.reporter.warning(msg, line=self.lineno)
 
-    def _record_name(self, name, target_id, signode):
+    def _record_name(self, name, target_id, signature: str, signode):
         """Record a `name` in the current subdomain, mapping it to `target_id`.
 
         Warns if another object of the same name already exists; `signode` is
@@ -230,19 +240,19 @@ def _record_name(self, name, target_id, signode):
         """
         names_in_subdomain = self.subdomain_data()
         self._warn_if_duplicate_name(names_in_subdomain, name, signode)
-        names_in_subdomain[name] = SubdomainItemData(self.env.docname, self.objtype, target_id)
+        names_in_subdomain[name] = SubdomainItemData(self.env.docname, self.objtype, target_id, self._signature_to_syntax(signature))
 
     def _target_id(self, name):
         return make_target(self.objtype, make_id(name))
 
-    def _add_target(self, signode, name):
+    def _add_target(self, signature: str, signode, name):
         """Register a link target ‘name’, pointing to signode."""
         targetid = self._target_id(name)
         if targetid not in self.state.document.ids:
             signode['ids'].append(targetid)
             signode['names'].append(name)
             signode['first'] = (not self.names)
-            self._record_name(name, targetid, signode)
+            self._record_name(name, targetid, signature, signode)
         else:
             # We don't warn for duplicates in the SSReflect chapter, because
             # it's the style of this chapter to repeat all the defined
@@ -261,14 +271,14 @@ def _add_index_entry(self, name, target):
             index_text += " " + self.index_suffix
         self.indexnode['entries'].append(('single', index_text, target, '', None))
 
-    def add_target_and_index(self, names, _, signode):
+    def add_target_and_index(self, names, signature: str, signode):
         """Attach a link target to `signode` and index entries for `names`.
         This is only called (from ``ObjectDescription.run``) if ``:noindex:`` isn't specified."""
         if names:
             for name in names:
                 if isinstance(name, str) and name.startswith('_'):
                     continue
-                target = self._add_target(signode, name)
+                target = self._add_target(signature, signode, name)
                 self._add_index_entry(name, target)
             self.state.document.note_explicit_target(signode)
 
@@ -328,6 +338,9 @@ class NotationObject(DocumentableObject):
     Objects that inherit from this class can use the notation grammar (“{+ …}”,
     “@…”, etc.) in their signature.
     """
+    def _signature_to_syntax(self, signature: str) -> list[object_notations.NotationObject]:
+        return object_notations.objectify(signature)
+
     def _render_signature(self, signature, signode):
         position = self.state_machine.get_source_and_line(self.lineno)
         tacn_node = notation_to_sphinx(signature, *position)
@@ -465,7 +478,7 @@ def _add_index_entry(self, name, target):
     def _target_id(self, name):
         return make_id('grammar-token-{}'.format(name[1]))
 
-    def _record_name(self, name, targetid, signode):
+    def _record_name(self, name, targetid, signature, signode):
         env = self.state.document.settings.env
         objects = env.domaindata['std']['objects']
         self._warn_if_duplicate_name(objects, name, signode)

From 5c62caae46cf72e47086e74c45acafc6481c3f1c Mon Sep 17 00:00:00 2001
From: shilangyu <xmarcinmarcin@gmail.com>
Date: Sun, 26 Apr 2026 17:33:51 +0200
Subject: [PATCH 06/28] doc: generate JSON indices

(cherry picked from commit bb201705f00086e68e5639fe359c4528080e0dab)
---
 .gitignore                            |  1 +
 Makefile                              |  7 ++-
 doc/README.md                         | 70 +++++++++++++++++++++++++++
 doc/tools/rocqrst/notations/object.py |  8 +--
 doc/tools/rocqrst/rocqdomain.py       | 34 +++++++++++++
 5 files changed, 115 insertions(+), 5 deletions(-)

diff --git a/.gitignore b/.gitignore
index 39c39c189743..829e0075be7c 100644
--- a/.gitignore
+++ b/.gitignore
@@ -107,6 +107,7 @@ result
 doc/unreleased.rst
 doc/refman-html
 doc/refman-pdf
+doc/refman-indices
 doc/common/version.tex
 doc/faq/html/
 doc/faq/axioms.eps
diff --git a/Makefile b/Makefile
index c604a4a5abd4..c0f3cef1caad 100644
--- a/Makefile
+++ b/Makefile
@@ -11,7 +11,7 @@
 # Dune Makefile for Rocq
 
 .PHONY: help help-install states world rocqide watch check    # Main developer targets
-.PHONY: refman-html refman-pdf corelib-html apidoc     # Documentation targets
+.PHONY: refman-html refman-pdf refman-indices corelib-html apidoc     # Documentation targets
 .PHONY: test-suite dev-targets
 .PHONY: fmt ocheck obuild ireport clean               # Maintenance targets
 .PHONY: dunestrap release install                 # Miscellaneous
@@ -63,6 +63,7 @@ help:
 	@echo ""
 	@echo "  - refman-html: build Rocq's reference manual [HTML version]"
 	@echo "  - refman-pdf:  build Rocq's reference manual [PDF version]"
+	@echo "  - refman-indices: build Rocq's JSON indices"
 	@echo "  - corelib-html: build Rocq's Corelib documentation [HTML version]"
 	@echo "  - apidoc:      build ML API documentation"
 	@echo ""
@@ -192,6 +193,10 @@ refman-pdf: world doc/unreleased.rst
 	+$(WITHPYPATH) $(WITHJOBS) dune exec -- sphinx-build -q -W -b latex doc/sphinx doc/refman-pdf
 	$(MAKE) -C doc/refman-pdf LATEXMKOPTS=-silent
 
+refman-indices: world doc/unreleased.rst
+	rm -rf doc/refman-indices
+	$(WITHPYPATH) dune exec -- sphinx-build -q -W -b dummy doc/sphinx doc/refman-indices
+
 corelib-html: dunestrap
 	dune build @corelib-html
 
diff --git a/doc/README.md b/doc/README.md
index ee32e0e56cf9..905999e50515 100644
--- a/doc/README.md
+++ b/doc/README.md
@@ -71,6 +71,73 @@ Or if you want to use less disk space:
     apt install texlive-latex-extra texlive-fonts-recommended texlive-xetex \
                 latexmk fonts-freefont-otf
 
+### JSON indices
+
+The documentation generator can also produce computer-readable JSON files for individual indices
+with `make refman-indices`. These files are meant to be useful for tool developers, for instance
+to power autocompletion in editors. They output files are found in `doc/refman-indices/*.json`.
+
+Each JSON index has the following shape:
+
+```typescript
+{
+  // a key is the name of the index entry
+  [string]: {
+    // the refman documentation page path for that entry
+    "documentation_path": string.
+    // the anchor on that page that leads to the documentation entry
+    "documentation_anchor": string,
+    // the grammar description
+    "syntax": Syntax
+  }
+}
+```
+
+Where `Syntax` can be used to match some text against the index entry or to propose the
+user a code snippet. It is of the following shape:
+
+```ts
+type Syntax =
+  | Literal
+  | Reference
+  | Alternative
+  | Repeat
+
+// the literal string
+type Literal = {
+  type: "literal"
+  value: string
+  // an optional subscript, for example "1" which should be rendered as "₁"
+  subscript: string | null
+}
+
+// a reference to a different entry in the documentation
+type Reference = {
+  type: "reference"
+  value: string
+  // an optional subscript, for example "1" which should be rendered as "₁"
+  subscript: string | null
+}
+
+// an alternative between a list of options
+type Alternative = {
+  type: "alternative"
+  children: Syntax[]
+}
+
+// repetition of a list of syntax nodes
+type Repeat = {
+  type: "repeat"
+  // nodes have to repeat at least this many times
+  min: number
+  // nodes can repeat up to and including this many times
+  max: number | null
+  // each repetition has to be separated with this
+  separator: string | null
+  children: Syntax[]
+}
+```
+
 ### Setting the locale for Python
 
 Make sure that the locale is configured on your platform so that Python encodes
@@ -106,6 +173,9 @@ The current documentation targets are:
 - `make corelib-html`
   Build Rocq core library documentation into `_build/default/doc/corelib/html`
 
+- `make refman-indices`
+  Build the JSON indices into `doc/refman-indices`
+
 - `make apidoc`
   Build the ML API's documentation into `_build/default/_doc/_html`
 
diff --git a/doc/tools/rocqrst/notations/object.py b/doc/tools/rocqrst/notations/object.py
index ce9b8f644426..b3e40d2ce307 100644
--- a/doc/tools/rocqrst/notations/object.py
+++ b/doc/tools/rocqrst/notations/object.py
@@ -13,18 +13,18 @@ def asdict(self):
 class Literal(NotationObject):
     value: str
     subscript: str | None
-    type = "literal"
+    type: str = "literal"
 
 @dataclass
 class Reference(NotationObject):
     value: str
     subscript: str | None
-    type = "reference"
+    type: str = "reference"
 
 @dataclass
 class Alternative(NotationObject):
     children: list[NotationObject]
-    type = "alternative"
+    type: str = "alternative"
 
 @dataclass
 class Repeat(NotationObject):
@@ -32,7 +32,7 @@ class Repeat(NotationObject):
     max: int | None
     separator: str | None
     children: list[NotationObject]
-    type = "repeat"
+    type: str = "repeat"
 
 class TacticNotationsToObjectVisitor(TacticNotationsVisitor):
     def defaultResult(self):
diff --git a/doc/tools/rocqrst/rocqdomain.py b/doc/tools/rocqrst/rocqdomain.py
index f7ed75f047c5..e30e0c9969b0 100644
--- a/doc/tools/rocqrst/rocqdomain.py
+++ b/doc/tools/rocqrst/rocqdomain.py
@@ -34,6 +34,7 @@
 from docutils.parsers.rst.directives.admonitions import BaseAdmonition
 
 from sphinx import addnodes, version_info as sphinx_version
+from sphinx.application import Sphinx
 from sphinx.directives import ObjectDescription
 from sphinx.domains import Domain, ObjType, Index
 from sphinx.errors import ExtensionError
@@ -1258,6 +1259,38 @@ def simplify_source_code_blocks_for_latex(app, doctree, fromdocname): # pylint:
         else:
             node.replace_self(nodes.literal_block(node.rawsource, node.rawsource, language="Coq"))
 
+def export_indices_to_json(app: Sphinx, exception):
+    """Write out JSON files containing the contents of our indices. This computer-readable format is
+    useful for tool developers, for instance to power autocompletion in editors.
+    """
+    import json
+
+    if app.builder.name != 'dummy':
+        return
+
+    if exception:
+        return
+
+    domain = app.env.get_domain('rocq')
+
+    def write_json(index: RocqSubdomainsIndex):
+        items = chain(*(domain.data['objects'][subdomain].items()
+                        for subdomain in index.subdomains))
+
+        output_data = {}
+        for name, data in items:
+            output_data[name] = {
+                "documentation_path": data.docname,
+                "documentation_anchor": data.targetid,
+                "syntax": [x.asdict() for x in data.syntax],
+            }
+
+        with open(app.outdir + f"/{index.name}.json", "w") as f:
+            json.dump(output_data, f, indent=2)
+
+    for index in RocqDomain.indices:
+        write_json(index)
+
 ROCQ_ADDITIONAL_DIRECTIVES = [RocqtopDirective,
                              RocqdocDirective,
                              ExampleDirective,
@@ -1291,6 +1324,7 @@ def setup(app):
     app.add_transform(RocqtopBlocksTransform)
     app.connect('doctree-resolved', simplify_source_code_blocks_for_latex)
     app.connect('doctree-resolved', RocqtopBlocksTransform.merge_consecutive_rocqtop_blocks)
+    app.connect('build-finished', export_indices_to_json)
 
     # Add extra styles
     app.add_css_file("ansi.css")

From 345389b7b4008cfad4de70089c44adb0d6692d9f Mon Sep 17 00:00:00 2001
From: shilangyu <xmarcinmarcin@gmail.com>
Date: Wed, 29 Apr 2026 21:57:57 +0200
Subject: [PATCH 07/28] doc: generate indices with custom builder

(cherry picked from commit af802980c8338e08ca5776f05dc2bf7c085de817)
---
 Makefile                        |  2 +-
 doc/README.md                   |  4 +-
 doc/tools/rocqrst/rocqdomain.py | 87 +++++++++++++++++++++------------
 3 files changed, 61 insertions(+), 32 deletions(-)

diff --git a/Makefile b/Makefile
index c0f3cef1caad..20d0bbadbd1f 100644
--- a/Makefile
+++ b/Makefile
@@ -195,7 +195,7 @@ refman-pdf: world doc/unreleased.rst
 
 refman-indices: world doc/unreleased.rst
 	rm -rf doc/refman-indices
-	$(WITHPYPATH) dune exec -- sphinx-build -q -W -b dummy doc/sphinx doc/refman-indices
+	$(WITHPYPATH) dune exec -- sphinx-build -q -W -b indices doc/sphinx doc/refman-indices
 
 corelib-html: dunestrap
 	dune build @corelib-html
diff --git a/doc/README.md b/doc/README.md
index 905999e50515..fc427f381855 100644
--- a/doc/README.md
+++ b/doc/README.md
@@ -88,7 +88,9 @@ Each JSON index has the following shape:
     // the anchor on that page that leads to the documentation entry
     "documentation_anchor": string,
     // the grammar description
-    "syntax": Syntax
+    "syntax": Syntax,
+    // a simpler, plain text documentation
+    "documentation": string,
   }
 }
 ```
diff --git a/doc/tools/rocqrst/rocqdomain.py b/doc/tools/rocqrst/rocqdomain.py
index e30e0c9969b0..5ff21d4d7002 100644
--- a/doc/tools/rocqrst/rocqdomain.py
+++ b/doc/tools/rocqrst/rocqdomain.py
@@ -21,6 +21,7 @@
 # pylint: disable=import-outside-toplevel, abstract-method, too-many-lines
 
 import os
+import json
 import re
 import shlex
 from itertools import chain
@@ -43,6 +44,7 @@
 from sphinx.util.logging import getLogger, get_node_location
 from sphinx.util.nodes import set_source_info, set_role_source_info, make_refnode
 from sphinx.writers.latex import LaTeXTranslator
+from sphinx.builders.text import TextBuilder
 
 from . import rocqdoc
 from .repl import ansicolors
@@ -1259,37 +1261,62 @@ def simplify_source_code_blocks_for_latex(app, doctree, fromdocname): # pylint:
         else:
             node.replace_self(nodes.literal_block(node.rawsource, node.rawsource, language="Coq"))
 
-def export_indices_to_json(app: Sphinx, exception):
-    """Write out JSON files containing the contents of our indices. This computer-readable format is
-    useful for tool developers, for instance to power autocompletion in editors.
-    """
-    import json
-
-    if app.builder.name != 'dummy':
-        return
-
-    if exception:
-        return
-
-    domain = app.env.get_domain('rocq')
 
-    def write_json(index: RocqSubdomainsIndex):
-        items = chain(*(domain.data['objects'][subdomain].items()
-                        for subdomain in index.subdomains))
+class IndicesBuilder(TextBuilder):
+    """Custom sphinx builder to generate JSON files containing the content of our indices.
+
+    It is based on the TextBuilder to be able to generate the content of the documentation for each object."""
+    name = 'indices'
+    format = 'json'
+    allow_parallel = True
+
+    def init(self):
+        super().init()
+        self.rendered: dict[str, str] = {}
+
+    def write_doc(self, docname: str, doctree: nodes.document) -> None:
+        domain = self.env.get_domain('rocq')
+        # find all nodes that are handled by our rocq domain
+        for node in doctree.findall(lambda n: isinstance(n, nodes.Element) and n.get('objtype') in domain.object_types):
+            # all IDs will be associated to this content
+            all_target_ids = []
+            for sig in node.traverse(addnodes.desc_signature):
+                all_target_ids.extend(sig.get('ids', []))
+
+            # the content is the next node
+            content_node = node.next_node(addnodes.desc_content)
+
+            if all_target_ids and content_node:
+                # translate sphinx nodes to text and associate it to all IDs
+                translator = self.create_translator(doctree, self)
+                translator.visit_document(content_node)
+                content_node.walkabout(translator)
+                translator.depart_document(content_node)
+                text = translator.body.strip()
+                for tid in all_target_ids:
+                    self.rendered[tid] = text
+
+    def finish(self):
+        domain = self.env.get_domain('rocq')
+
+        def write_json(index: RocqSubdomainsIndex):
+            items = chain(*(domain.data['objects'][subdomain].items()
+                            for subdomain in index.subdomains))
+
+            output_data = {}
+            for name, data in items:
+                output_data[name] = {
+                    "documentation_path": data.docname,
+                    "documentation_anchor": data.targetid,
+                    "syntax": [x.asdict() for x in data.syntax],
+                    "documentation": self.rendered.get(data.targetid, "")
+                }
+
+            with open(self.outdir / f"{index.name}.json", "w") as f:
+                json.dump(output_data, f, indent=2)
 
-        output_data = {}
-        for name, data in items:
-            output_data[name] = {
-                "documentation_path": data.docname,
-                "documentation_anchor": data.targetid,
-                "syntax": [x.asdict() for x in data.syntax],
-            }
-
-        with open(app.outdir + f"/{index.name}.json", "w") as f:
-            json.dump(output_data, f, indent=2)
-
-    for index in RocqDomain.indices:
-        write_json(index)
+        for index in RocqDomain.indices:
+            write_json(index)
 
 ROCQ_ADDITIONAL_DIRECTIVES = [RocqtopDirective,
                              RocqdocDirective,
@@ -1313,6 +1340,7 @@ def setup(app):
 
     # Add domain, directives, and roles
     app.add_domain(RocqDomain)
+    app.add_builder(IndicesBuilder)
     app.add_index_to_domain('std', StdGlossaryIndex)
 
     for role in ROCQ_ADDITIONAL_ROLES:
@@ -1324,7 +1352,6 @@ def setup(app):
     app.add_transform(RocqtopBlocksTransform)
     app.connect('doctree-resolved', simplify_source_code_blocks_for_latex)
     app.connect('doctree-resolved', RocqtopBlocksTransform.merge_consecutive_rocqtop_blocks)
-    app.connect('build-finished', export_indices_to_json)
 
     # Add extra styles
     app.add_css_file("ansi.css")

From c23dba5b475800cd1c58ff73ad1973f68fdde248 Mon Sep 17 00:00:00 2001
From: shilangyu <xmarcinmarcin@gmail.com>
Date: Sat, 16 May 2026 21:07:29 +0200
Subject: [PATCH 08/28] doc: encode data unions in indices in an outer manner

(cherry picked from commit f93ea0f8c45c755513a125068e2e709ae0404a1a)
---
 doc/README.md                         | 12 +++----
 doc/tools/rocqrst/notations/object.py | 47 +++++++++++++++++----------
 doc/tools/rocqrst/rocqdomain.py       | 12 +++----
 3 files changed, 39 insertions(+), 32 deletions(-)

diff --git a/doc/README.md b/doc/README.md
index fc427f381855..913d791259f5 100644
--- a/doc/README.md
+++ b/doc/README.md
@@ -100,14 +100,13 @@ user a code snippet. It is of the following shape:
 
 ```ts
 type Syntax =
-  | Literal
-  | Reference
-  | Alternative
-  | Repeat
+  | ["Literal", Literal]
+  | ["Reference", Reference]
+  | ["Alternative", Alternative]
+  | ["Repeat", Repeat]
 
 // the literal string
 type Literal = {
-  type: "literal"
   value: string
   // an optional subscript, for example "1" which should be rendered as "₁"
   subscript: string | null
@@ -115,7 +114,6 @@ type Literal = {
 
 // a reference to a different entry in the documentation
 type Reference = {
-  type: "reference"
   value: string
   // an optional subscript, for example "1" which should be rendered as "₁"
   subscript: string | null
@@ -123,13 +121,11 @@ type Reference = {
 
 // an alternative between a list of options
 type Alternative = {
-  type: "alternative"
   children: Syntax[]
 }
 
 // repetition of a list of syntax nodes
 type Repeat = {
-  type: "repeat"
   // nodes have to repeat at least this many times
   min: number
   // nodes can repeat up to and including this many times
diff --git a/doc/tools/rocqrst/notations/object.py b/doc/tools/rocqrst/notations/object.py
index b3e40d2ce307..170bd54ceba0 100644
--- a/doc/tools/rocqrst/notations/object.py
+++ b/doc/tools/rocqrst/notations/object.py
@@ -1,4 +1,5 @@
 from dataclasses import asdict, dataclass
+from typing import Self
 
 from .parsing import parse
 from .TacticNotationsParser import TacticNotationsParser
@@ -9,30 +10,40 @@ class NotationObject:
     def asdict(self):
         return asdict(self)
 
+TaggedNotationObject = tuple[str, NotationObject]
+
 @dataclass
 class Literal(NotationObject):
     value: str
     subscript: str | None
-    type: str = "literal"
+    @classmethod
+    def new(cls, value: Self) -> tuple[str, Self]:
+        return ("Literal", value)
 
 @dataclass
 class Reference(NotationObject):
     value: str
     subscript: str | None
-    type: str = "reference"
+    @classmethod
+    def new(cls, value: Self) -> tuple[str, Self]:
+        return ("Reference", value)
 
 @dataclass
 class Alternative(NotationObject):
-    children: list[NotationObject]
-    type: str = "alternative"
+    children: list[TaggedNotationObject]
+    @classmethod
+    def new(cls, value: Self) -> tuple[str, Self]:
+        return ("Alternative", value)
 
 @dataclass
 class Repeat(NotationObject):
     min: int
     max: int | None
     separator: str | None
-    children: list[NotationObject]
-    type: str = "repeat"
+    children: list[TaggedNotationObject]
+    @classmethod
+    def new(cls, value: Self) -> tuple[str, Self]:
+        return ("Repeat", value)
 
 class TacticNotationsToObjectVisitor(TacticNotationsVisitor):
     def defaultResult(self):
@@ -48,7 +59,7 @@ def aggregateResult(self, aggregate, nextResult):
         return aggregate
 
     def visitAlternative(self, ctx: TacticNotationsParser.AlternativeContext):
-        return [Alternative(children=self.visitChildren(ctx))]
+        return [Alternative.new(Alternative(children=self.visitChildren(ctx)))]
 
     def visitAltblock(self, ctx: TacticNotationsParser.AltblockContext):
         return self.visitChildren(ctx)
@@ -69,40 +80,40 @@ def visitRepeat(self, ctx: TacticNotationsParser.RepeatContext):
             case _:
                 raise ValueError(f"Unexpected repeat marker: {repeat_marker}")
 
-        return [Repeat(
+        return [Repeat.new(Repeat(
             min=min_rep,
             max=max_rep,
             separator=separator.getText() if separator else None,
             children=self.visitChildren(ctx)
-        )]
+        ))]
 
     def visitCurlies(self, ctx: TacticNotationsParser.CurliesContext):
         return [
-            Literal(value=ctx.LBRACE().getText(), subscript=None),
+            Literal.new(Literal(value=ctx.LBRACE().getText(), subscript=None)),
             *self.visitChildren(ctx),
-            Literal(value=ctx.RBRACE().getText(), subscript=None)]
+            Literal.new(Literal(value=ctx.RBRACE().getText(), subscript=None))]
 
     def visitAtomic(self, ctx: TacticNotationsParser.AtomicContext):
-        return [Literal(
+        return [Literal.new(Literal(
             value=ctx.ATOM().getText(),
             # skip '__'
             subscript=ctx.SUB().getText()[2:] if ctx.SUB() else None
-        )]
+        ))]
 
     def visitHole(self, ctx: TacticNotationsParser.HoleContext):
-        return [Reference(
+        return [Reference.new(Reference(
             value=ctx.ID().getText()[1:],
             # skip '__'
             subscript=ctx.SUB().getText()[2:] if ctx.SUB() else None
-        )]
+        ))]
 
     def visitEscaped(self, ctx: TacticNotationsParser.EscapedContext):
-        return [Literal(
+        return [Literal.new(Literal(
             value=ctx.ESCAPED().getText().replace("%", ""),
             subscript=None
-        )]
+        ))]
 
-def objectify(notation: str) -> list[NotationObject]:
+def objectify(notation: str) -> list[TaggedNotationObject]:
     """Translate a notation into an object.
 
     It is essentially a simplified and normalized version of the ANTLR AST.
diff --git a/doc/tools/rocqrst/rocqdomain.py b/doc/tools/rocqrst/rocqdomain.py
index 5ff21d4d7002..08e7c7225438 100644
--- a/doc/tools/rocqrst/rocqdomain.py
+++ b/doc/tools/rocqrst/rocqdomain.py
@@ -95,7 +95,7 @@ class SubdomainItemData:
     docname: str
     objtype: str
     targetid: str
-    syntax: list[object_notations.NotationObject]
+    syntax: list[object_notations.TaggedNotationObject]
 
 def notation_to_sphinx(notation, source, line, rawtext=None):
     """Parse notation and wrap it in an inline node"""
@@ -183,13 +183,13 @@ def _render_signature(self, signature, signode):
         """Render a signature, placing resulting nodes into signode."""
         raise NotImplementedError(self)
 
-    def _signature_to_syntax(self, signature: str) -> list[object_notations.NotationObject]:
+    def _signature_to_syntax(self, signature: str) -> list[object_notations.TaggedNotationObject]:
         """Convert a signature into a syntax tree, used in generated plain JSON indices.
 
         By default, returns the signature as a literal string.
 
         """
-        return [object_notations.Literal(value=signature, subscript=None)]
+        return [object_notations.Literal.new(object_notations.Literal(value=signature, subscript=None))]
 
     option_spec = {
         # Explicit object naming
@@ -341,7 +341,7 @@ class NotationObject(DocumentableObject):
     Objects that inherit from this class can use the notation grammar (“{+ …}”,
     “@…”, etc.) in their signature.
     """
-    def _signature_to_syntax(self, signature: str) -> list[object_notations.NotationObject]:
+    def _signature_to_syntax(self, signature: str) -> list[object_notations.TaggedNotationObject]:
         return object_notations.objectify(signature)
 
     def _render_signature(self, signature, signode):
@@ -1300,7 +1300,7 @@ def finish(self):
         domain = self.env.get_domain('rocq')
 
         def write_json(index: RocqSubdomainsIndex):
-            items = chain(*(domain.data['objects'][subdomain].items()
+            items: list[tuple[str, SubdomainItemData]] = chain(*(domain.data['objects'][subdomain].items()
                             for subdomain in index.subdomains))
 
             output_data = {}
@@ -1308,7 +1308,7 @@ def write_json(index: RocqSubdomainsIndex):
                 output_data[name] = {
                     "documentation_path": data.docname,
                     "documentation_anchor": data.targetid,
-                    "syntax": [x.asdict() for x in data.syntax],
+                    "syntax": [[x[0], x[1].asdict()] for x in data.syntax],
                     "documentation": self.rendered.get(data.targetid, "")
                 }
 

From 5f172c95d7a8bc606eca9b36bdf585c85866319f Mon Sep 17 00:00:00 2001
From: shilangyu <xmarcinmarcin@gmail.com>
Date: Sun, 5 Jul 2026 13:23:05 +0200
Subject: [PATCH 09/28] doc: update makefile indices generation

(cherry picked from commit 36040ea013b72265cd762c6eaf830912ee253dd1)
---
 Makefile | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Makefile b/Makefile
index 20d0bbadbd1f..f50763ef674a 100644
--- a/Makefile
+++ b/Makefile
@@ -195,7 +195,7 @@ refman-pdf: world doc/unreleased.rst
 
 refman-indices: world doc/unreleased.rst
 	rm -rf doc/refman-indices
-	$(WITHPYPATH) dune exec -- sphinx-build -q -W -b indices doc/sphinx doc/refman-indices
+	+$(WITHPYPATH) $(WITHJOBS) dune exec -- sphinx-build -q -W -b indices doc/sphinx doc/refman-indices
 
 corelib-html: dunestrap
 	dune build @corelib-html

From 56ac39cff69153d509262e47aa720410aa431fad Mon Sep 17 00:00:00 2001
From: shilangyu <xmarcinmarcin@gmail.com>
Date: Sun, 5 Jul 2026 13:30:01 +0200
Subject: [PATCH 10/28] doc: shim usage of the Self type

(cherry picked from commit 02a9f7a7ef8cfe168492692dbe3de0b2de861cd9)
---
 doc/tools/rocqrst/notations/object.py | 14 +++++++++-----
 1 file changed, 9 insertions(+), 5 deletions(-)

diff --git a/doc/tools/rocqrst/notations/object.py b/doc/tools/rocqrst/notations/object.py
index 170bd54ceba0..e5d591a4d903 100644
--- a/doc/tools/rocqrst/notations/object.py
+++ b/doc/tools/rocqrst/notations/object.py
@@ -1,5 +1,5 @@
 from dataclasses import asdict, dataclass
-from typing import Self
+from typing import TypeVar
 
 from .parsing import parse
 from .TacticNotationsParser import TacticNotationsParser
@@ -12,29 +12,33 @@ def asdict(self):
 
 TaggedNotationObject = tuple[str, NotationObject]
 
+SelfLiteral = TypeVar("Self", bound="Literal")
 @dataclass
 class Literal(NotationObject):
     value: str
     subscript: str | None
     @classmethod
-    def new(cls, value: Self) -> tuple[str, Self]:
+    def new(cls, value: SelfLiteral) -> tuple[str, SelfLiteral]:
         return ("Literal", value)
 
+SelfReference = TypeVar("Self", bound="Reference")
 @dataclass
 class Reference(NotationObject):
     value: str
     subscript: str | None
     @classmethod
-    def new(cls, value: Self) -> tuple[str, Self]:
+    def new(cls, value: SelfReference) -> tuple[str, SelfReference]:
         return ("Reference", value)
 
+SelfAlternative = TypeVar("Self", bound="Alternative")
 @dataclass
 class Alternative(NotationObject):
     children: list[TaggedNotationObject]
     @classmethod
-    def new(cls, value: Self) -> tuple[str, Self]:
+    def new(cls, value: SelfAlternative) -> tuple[str, SelfAlternative]:
         return ("Alternative", value)
 
+SelfRepeat = TypeVar("Self", bound="Repeat")
 @dataclass
 class Repeat(NotationObject):
     min: int
@@ -42,7 +46,7 @@ class Repeat(NotationObject):
     separator: str | None
     children: list[TaggedNotationObject]
     @classmethod
-    def new(cls, value: Self) -> tuple[str, Self]:
+    def new(cls, value: SelfRepeat) -> tuple[str, SelfRepeat]:
         return ("Repeat", value)
 
 class TacticNotationsToObjectVisitor(TacticNotationsVisitor):

From a595d3710739b2f2dbd9684ec1f37a97fba87eaa Mon Sep 17 00:00:00 2001
From: shilangyu <xmarcinmarcin@gmail.com>
Date: Sun, 5 Jul 2026 15:12:43 +0200
Subject: [PATCH 11/28] doc: allow single underscores in ATOM

This makes sure to avoid conflicts with SUB which works only whenever there are two consecutive underscores. But in return things like `setoid_rewrite` will be seen as a single token (as it should).

(cherry picked from commit 2a6c43fbed9d06f7f5f6568135102e5457f7c342)
---
 doc/tools/rocqrst/notations/TacticNotations.g |  2 +-
 .../rocqrst/notations/TacticNotationsLexer.py | 35 ++++++++++---------
 2 files changed, 20 insertions(+), 17 deletions(-)

diff --git a/doc/tools/rocqrst/notations/TacticNotations.g b/doc/tools/rocqrst/notations/TacticNotations.g
index ef6b633173a6..446fae0ecef5 100644
--- a/doc/tools/rocqrst/notations/TacticNotations.g
+++ b/doc/tools/rocqrst/notations/TacticNotations.g
@@ -46,7 +46,7 @@ RBRACE: '}';
 ESCAPED: '%{' | '%}' | '%|' | '`%{' | '@%{' |
   '%|-' | '%|->' | '%||' | '%|||' | '%||||';  // for SSR
 PIPE: '|';
-ATOM: '@' | '_' | ~[@_{}| ]+;
+ATOM: '@' | '_' | ~[@_{}| ]+ ('_' ~[@_{}| ]+)*;
 ID: '@' ('_'? [a-zA-Z0-9])+;
 SUB: '_' '_' [a-zA-Z0-9]+;
 WHITESPACE: ' '+;
diff --git a/doc/tools/rocqrst/notations/TacticNotationsLexer.py b/doc/tools/rocqrst/notations/TacticNotationsLexer.py
index f143a87a4965..ce455af5488e 100644
--- a/doc/tools/rocqrst/notations/TacticNotationsLexer.py
+++ b/doc/tools/rocqrst/notations/TacticNotationsLexer.py
@@ -8,21 +8,22 @@
 def serializedATN():
     with StringIO() as buf:
         buf.write("\3\u608b\ua72a\u8133\ub9ed\u417c\u3be7\u7786\u5964\2\f")
-        buf.write("f\b\1\4\2\t\2\4\3\t\3\4\4\t\4\4\5\t\5\4\6\t\6\4\7\t\7")
+        buf.write("q\b\1\4\2\t\2\4\3\t\3\4\4\t\4\4\5\t\5\4\6\t\6\4\7\t\7")
         buf.write("\4\b\t\b\4\t\t\t\4\n\t\n\4\13\t\13\3\2\3\2\3\2\3\3\3\3")
         buf.write("\3\3\3\3\3\3\3\3\5\3!\n\3\3\4\3\4\3\5\3\5\3\6\3\6\3\6")
         buf.write("\3\6\3\6\3\6\3\6\3\6\3\6\3\6\3\6\3\6\3\6\3\6\3\6\3\6\3")
         buf.write("\6\3\6\3\6\3\6\3\6\3\6\3\6\3\6\3\6\3\6\3\6\3\6\3\6\3\6")
-        buf.write("\3\6\5\6F\n\6\3\7\3\7\3\b\3\b\6\bL\n\b\r\b\16\bM\5\bP")
-        buf.write("\n\b\3\t\3\t\5\tT\n\t\3\t\6\tW\n\t\r\t\16\tX\3\n\3\n\3")
-        buf.write("\n\6\n^\n\n\r\n\16\n_\3\13\6\13c\n\13\r\13\16\13d\2\2")
-        buf.write("\f\3\3\5\4\7\5\t\6\13\7\r\b\17\t\21\n\23\13\25\f\3\2\5")
-        buf.write("\4\2BBaa\6\2\"\"BBaa}\177\5\2\62;C\\c|\2v\2\3\3\2\2\2")
+        buf.write("\3\6\5\6F\n\6\3\7\3\7\3\b\3\b\6\bL\n\b\r\b\16\bM\3\b\3")
+        buf.write("\b\6\bR\n\b\r\b\16\bS\7\bV\n\b\f\b\16\bY\13\b\5\b[\n\b")
+        buf.write("\3\t\3\t\5\t_\n\t\3\t\6\tb\n\t\r\t\16\tc\3\n\3\n\3\n\6")
+        buf.write("\ni\n\n\r\n\16\nj\3\13\6\13n\n\13\r\13\16\13o\2\2\f\3")
+        buf.write("\3\5\4\7\5\t\6\13\7\r\b\17\t\21\n\23\13\25\f\3\2\5\4\2")
+        buf.write("BBaa\6\2\"\"BBaa}\177\5\2\62;C\\c|\2\u0083\2\3\3\2\2\2")
         buf.write("\2\5\3\2\2\2\2\7\3\2\2\2\2\t\3\2\2\2\2\13\3\2\2\2\2\r")
         buf.write("\3\2\2\2\2\17\3\2\2\2\2\21\3\2\2\2\2\23\3\2\2\2\2\25\3")
         buf.write("\2\2\2\3\27\3\2\2\2\5 \3\2\2\2\7\"\3\2\2\2\t$\3\2\2\2")
-        buf.write("\13E\3\2\2\2\rG\3\2\2\2\17O\3\2\2\2\21Q\3\2\2\2\23Z\3")
-        buf.write("\2\2\2\25b\3\2\2\2\27\30\7}\2\2\30\31\7~\2\2\31\4\3\2")
+        buf.write("\13E\3\2\2\2\rG\3\2\2\2\17Z\3\2\2\2\21\\\3\2\2\2\23e\3")
+        buf.write("\2\2\2\25m\3\2\2\2\27\30\7}\2\2\30\31\7~\2\2\31\4\3\2")
         buf.write("\2\2\32\33\7}\2\2\33!\7-\2\2\34\35\7}\2\2\35!\7,\2\2\36")
         buf.write("\37\7}\2\2\37!\7A\2\2 \32\3\2\2\2 \34\3\2\2\2 \36\3\2")
         buf.write("\2\2!\6\3\2\2\2\"#\7}\2\2#\b\3\2\2\2$%\7\177\2\2%\n\3")
@@ -34,14 +35,16 @@ def serializedATN():
         buf.write("~\2\2?F\7~\2\2@A\7\'\2\2AB\7~\2\2BC\7~\2\2CD\7~\2\2DF")
         buf.write("\7~\2\2E&\3\2\2\2E(\3\2\2\2E*\3\2\2\2E,\3\2\2\2E/\3\2")
         buf.write("\2\2E\62\3\2\2\2E\65\3\2\2\2E9\3\2\2\2E<\3\2\2\2E@\3\2")
-        buf.write("\2\2F\f\3\2\2\2GH\7~\2\2H\16\3\2\2\2IP\t\2\2\2JL\n\3\2")
-        buf.write("\2KJ\3\2\2\2LM\3\2\2\2MK\3\2\2\2MN\3\2\2\2NP\3\2\2\2O")
-        buf.write("I\3\2\2\2OK\3\2\2\2P\20\3\2\2\2QV\7B\2\2RT\7a\2\2SR\3")
-        buf.write("\2\2\2ST\3\2\2\2TU\3\2\2\2UW\t\4\2\2VS\3\2\2\2WX\3\2\2")
-        buf.write("\2XV\3\2\2\2XY\3\2\2\2Y\22\3\2\2\2Z[\7a\2\2[]\7a\2\2\\")
-        buf.write("^\t\4\2\2]\\\3\2\2\2^_\3\2\2\2_]\3\2\2\2_`\3\2\2\2`\24")
-        buf.write("\3\2\2\2ac\7\"\2\2ba\3\2\2\2cd\3\2\2\2db\3\2\2\2de\3\2")
-        buf.write("\2\2e\26\3\2\2\2\13\2 EMOSX_d\2")
+        buf.write("\2\2F\f\3\2\2\2GH\7~\2\2H\16\3\2\2\2I[\t\2\2\2JL\n\3\2")
+        buf.write("\2KJ\3\2\2\2LM\3\2\2\2MK\3\2\2\2MN\3\2\2\2NW\3\2\2\2O")
+        buf.write("Q\7a\2\2PR\n\3\2\2QP\3\2\2\2RS\3\2\2\2SQ\3\2\2\2ST\3\2")
+        buf.write("\2\2TV\3\2\2\2UO\3\2\2\2VY\3\2\2\2WU\3\2\2\2WX\3\2\2\2")
+        buf.write("X[\3\2\2\2YW\3\2\2\2ZI\3\2\2\2ZK\3\2\2\2[\20\3\2\2\2\\")
+        buf.write("a\7B\2\2]_\7a\2\2^]\3\2\2\2^_\3\2\2\2_`\3\2\2\2`b\t\4")
+        buf.write("\2\2a^\3\2\2\2bc\3\2\2\2ca\3\2\2\2cd\3\2\2\2d\22\3\2\2")
+        buf.write("\2ef\7a\2\2fh\7a\2\2gi\t\4\2\2hg\3\2\2\2ij\3\2\2\2jh\3")
+        buf.write("\2\2\2jk\3\2\2\2k\24\3\2\2\2ln\7\"\2\2ml\3\2\2\2no\3\2")
+        buf.write("\2\2om\3\2\2\2op\3\2\2\2p\26\3\2\2\2\r\2 EMSWZ^cjo\2")
         return buf.getvalue()
 
 

From 0ee79f970c42b10f852b9ad7b42679d61979ce66 Mon Sep 17 00:00:00 2001
From: shilangyu <xmarcinmarcin@gmail.com>
Date: Sun, 5 Jul 2026 19:33:24 +0200
Subject: [PATCH 12/28] doc: generate proper markdown as indices docs

(cherry picked from commit debc670a99847f6d67f22b5fb32911175167967c)
---
 doc/README.md                   |  6 ++--
 doc/sphinx/conf.py              |  1 +
 doc/tools/rocqrst/rocqdomain.py | 54 +++++++++++++++++++++++++++------
 3 files changed, 50 insertions(+), 11 deletions(-)

diff --git a/doc/README.md b/doc/README.md
index 913d791259f5..aaf5ebc8848d 100644
--- a/doc/README.md
+++ b/doc/README.md
@@ -36,12 +36,14 @@ reference manual requires Python 3, and the following Python packages:
   - antlr4-python3-runtime >= 4.7.1 & <= 4.9.3
   - pexpect >= 4.8.0
   - sphinxcontrib-bibtex >= 2.4.2
+  - sphinx-markdown-builder >= 0.6.10
 
 To install them, you should first install pip and setuptools (for instance,
 with `apt install python3-pip python3-setuptools` on Debian / Ubuntu) then run:
 
     pip3 install sphinx sphinx_rtd_theme beautifulsoup4 \
-                 antlr4-python3-runtime==4.7.1 pexpect sphinxcontrib-bibtex
+                 antlr4-python3-runtime==4.7.1 pexpect sphinxcontrib-bibtex \
+                 sphinx-markdown-builder==0.6.10
 
 Nix users should get the correct development environment to build the
 HTML documentation from Coq's [`default.nix`](../default.nix) (note this
@@ -89,7 +91,7 @@ Each JSON index has the following shape:
     "documentation_anchor": string,
     // the grammar description
     "syntax": Syntax,
-    // a simpler, plain text documentation
+    // a simpler, markdown documentation
     "documentation": string,
   }
 }
diff --git a/doc/sphinx/conf.py b/doc/sphinx/conf.py
index 2c20e1860093..a7c9dafe0a1c 100644
--- a/doc/sphinx/conf.py
+++ b/doc/sphinx/conf.py
@@ -60,6 +60,7 @@
     'sphinx.ext.mathjax',
     'sphinx.ext.todo',
     'sphinxcontrib.bibtex',
+    'sphinx_markdown_builder',
     'rocqrst.rocqdomain'
 ]
 
diff --git a/doc/tools/rocqrst/rocqdomain.py b/doc/tools/rocqrst/rocqdomain.py
index 08e7c7225438..f60e3886f41b 100644
--- a/doc/tools/rocqrst/rocqdomain.py
+++ b/doc/tools/rocqrst/rocqdomain.py
@@ -45,6 +45,8 @@
 from sphinx.util.nodes import set_source_info, set_role_source_info, make_refnode
 from sphinx.writers.latex import LaTeXTranslator
 from sphinx.builders.text import TextBuilder
+from sphinx_markdown_builder.translator import MarkdownTranslator, pushing_context
+from sphinx_markdown_builder.contexts import WrappedContext
 
 from . import rocqdoc
 from .repl import ansicolors
@@ -1261,6 +1263,39 @@ def simplify_source_code_blocks_for_latex(app, doctree, fromdocname): # pylint:
         else:
             node.replace_self(nodes.literal_block(node.rawsource, node.rawsource, language="Coq"))
 
+class IndicesMarkdownTranslator(MarkdownTranslator):
+    @pushing_context
+    def visit_caution(self, _node):
+        self._push_box("CAUTION")
+
+    def visit_admonition(self, node):
+        self.add('\n\n')
+    def depart_admonition(self, node):
+        self.add('\n\n')
+
+    # we do not create links in markdown
+    def visit_reference(self, node):
+        pass
+    def visit_download_reference(self, node):
+        pass
+
+
+    @pushing_context
+    def visit_desc_annotation(self, node):
+        text = node.astext().strip()
+        if text == "Error":
+            self.add("*Possible error*:")
+            raise nodes.SkipNode
+        elif text == "Warning":
+            self.add("*Possible warning*:")
+            raise nodes.SkipNode
+        self._push_context(WrappedContext("_"))
+
+    def visit_subscript(self, node):
+        self.add('(')
+    def depart_subscript(self, node):
+        self.add(')')
+
 
 class IndicesBuilder(TextBuilder):
     """Custom sphinx builder to generate JSON files containing the content of our indices.
@@ -1268,7 +1303,9 @@ class IndicesBuilder(TextBuilder):
     It is based on the TextBuilder to be able to generate the content of the documentation for each object."""
     name = 'indices'
     format = 'json'
-    allow_parallel = True
+    allow_parallel = False
+
+    default_translator_class = IndicesMarkdownTranslator
 
     def init(self):
         super().init()
@@ -1289,17 +1326,19 @@ def write_doc(self, docname: str, doctree: nodes.document) -> None:
             if all_target_ids and content_node:
                 # translate sphinx nodes to text and associate it to all IDs
                 translator = self.create_translator(doctree, self)
-                translator.visit_document(content_node)
+                translator.visit_document(doctree)
                 content_node.walkabout(translator)
-                translator.depart_document(content_node)
-                text = translator.body.strip()
+                translator.depart_document(doctree)
+                text = translator.astext().strip()
+                # remove some leftover formatting
+                text = text.replace('\u200b', '|').replace('\\\\textquotesingle{}', "").replace('\\textquotesingle{}', "")
                 for tid in all_target_ids:
                     self.rendered[tid] = text
 
     def finish(self):
         domain = self.env.get_domain('rocq')
 
-        def write_json(index: RocqSubdomainsIndex):
+        for index in RocqDomain.indices:
             items: list[tuple[str, SubdomainItemData]] = chain(*(domain.data['objects'][subdomain].items()
                             for subdomain in index.subdomains))
 
@@ -1308,16 +1347,13 @@ def write_json(index: RocqSubdomainsIndex):
                 output_data[name] = {
                     "documentation_path": data.docname,
                     "documentation_anchor": data.targetid,
-                    "syntax": [[x[0], x[1].asdict()] for x in data.syntax],
+                    "syntax": [[tag, notation.asdict()] for [tag, notation] in data.syntax],
                     "documentation": self.rendered.get(data.targetid, "")
                 }
 
             with open(self.outdir / f"{index.name}.json", "w") as f:
                 json.dump(output_data, f, indent=2)
 
-        for index in RocqDomain.indices:
-            write_json(index)
-
 ROCQ_ADDITIONAL_DIRECTIVES = [RocqtopDirective,
                              RocqdocDirective,
                              ExampleDirective,

From bc4c460b57ceacf361be9bc69f2382b421cafdaf Mon Sep 17 00:00:00 2001
From: shilangyu <xmarcinmarcin@gmail.com>
Date: Mon, 6 Jul 2026 14:13:34 +0200
Subject: [PATCH 13/28] docker: update ubuntu deps

(cherry picked from commit a511e40837c7ce38ce4aa27eaa10dbf618fc91f4)
---
 .gitlab-ci.yml                          | 4 ++--
 dev/ci/docker/edge_ubuntu/Dockerfile    | 2 +-
 dev/ci/docker/old_ubuntu_lts/Dockerfile | 7 ++++++-
 3 files changed, 9 insertions(+), 4 deletions(-)

diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index a1a7176caf64..784c6a9ed9d1 100644
--- a/.gitlab-ci.yml
+++ b/.gitlab-ci.yml
@@ -40,8 +40,8 @@ variables:
   # The $hash is the first 10 characters of the md5 of the Dockerfile. e.g.
   # echo $(md5sum dev/ci/docker/old_ubuntu_lts/Dockerfile | head -c 10)
   # echo $(md5sum dev/ci/docker/edge_ubuntu/Dockerfile | head -c 10)
-  BASE_CACHEKEY: "old_ubuntu_lts-V2026-06-10-d4125f9d9e"
-  EDGE_CACHEKEY: "edge_ubuntu-V2026-06-10-0c389ac2f4"
+  BASE_CACHEKEY: "old_ubuntu_lts-V2026-07-06-00242ff07f"
+  EDGE_CACHEKEY: "edge_ubuntu-V2026-07-06-62b9804f8c"
   BASE_IMAGE: "$CI_REGISTRY_IMAGE:$BASE_CACHEKEY"
   EDGE_IMAGE: "$CI_REGISTRY_IMAGE:$EDGE_CACHEKEY"
 
diff --git a/dev/ci/docker/edge_ubuntu/Dockerfile b/dev/ci/docker/edge_ubuntu/Dockerfile
index 44797ac4e68d..8d0e0697e360 100644
--- a/dev/ci/docker/edge_ubuntu/Dockerfile
+++ b/dev/ci/docker/edge_ubuntu/Dockerfile
@@ -36,7 +36,7 @@ RUN apt-get update -qq && apt-get install --no-install-recommends -y -qq \
 
 # More dependencies of the sphinx doc
 RUN pip3 install --break-system-packages docutils==0.21.2 sphinx==8.2.3 sphinx_rtd_theme==3.0.2 \
-        antlr4-python3-runtime==4.7.1 sphinxcontrib-bibtex==2.6.3 \
+        antlr4-python3-runtime==4.7.1 sphinxcontrib-bibtex==2.6.3 sphinx-markdown-builder==0.6.10 \
       && rm -rf ~/.cache/pip
 
 # We need to install OPAM 2.0 manually for now.
diff --git a/dev/ci/docker/old_ubuntu_lts/Dockerfile b/dev/ci/docker/old_ubuntu_lts/Dockerfile
index cf915236ea7e..2626e66b3b01 100644
--- a/dev/ci/docker/old_ubuntu_lts/Dockerfile
+++ b/dev/ci/docker/old_ubuntu_lts/Dockerfile
@@ -21,7 +21,7 @@ RUN apt-get update -qq && apt-get install --no-install-recommends -y -qq \
         texlive-latex-extra texlive-fonts-recommended texlive-xetex latexmk \
         python3-sphinx python3-docutils python3-sphinx-rtd-theme \
         python3-antlr4 python3-sphinxcontrib.bibtex \
-        python3-setuptools python3-pexpect python3-bs4 fonts-freefont-otf \
+        python3-pip python3-setuptools python3-pexpect python3-bs4 fonts-freefont-otf \
         # Dependency of stdlib-doc
         graphviz \
         # Dependencies of source-doc and coq-makefile
@@ -34,6 +34,11 @@ RUN apt-get update -qq && apt-get install --no-install-recommends -y -qq \
         python3-venv \
       && rm -rf /var/lib/apt/lists /usr/share/doc
 
+# More dependencies of the sphinx doc
+RUN pip3 install sphinx-markdown-builder==0.6.10 \
+      && rm -rf ~/.cache/pip
+
+
 # We need to install OPAM 2.0 manually for now.
 RUN wget https://github.com/ocaml/opam/releases/download/2.0.6/opam-2.0.6-x86_64-linux -O /usr/bin/opam && chmod 755 /usr/bin/opam
 

From 14888e36682985bcddd8f102b3f47001c416d6b3 Mon Sep 17 00:00:00 2001
From: Jason Gross <jason@theorem.dev>
Date: Mon, 6 Jul 2026 23:24:10 +0000
Subject: [PATCH 14/28] Fix #22220: do not bake template universes into
 rewriting schemes

The scheme builders in tactics/eqschemes.ml (Scheme Rewriting and the
congr scheme) substituted the default template levels (e.g. eq.u0) into
the contexts copied from the inductive declaration, so the types of
eq_sym, eq_sym_involutive and eq_rew_r_dep mentioned Type@{eq.u0}.
Using these constants at any fresh universe would then constrain the
global template universe, which is flagged by bad-template-constraint;
with Set Warnings "+bad-template-constraint", even eta-expanding
eq_sym failed:

    Check (fun x => @eq_sym x).
    (* Error: Adding constraints involving global template univs:
       test.22 <= eq.u0 *)

Instead, instantiate the template context with fresh levels declared as
universes of the scheme: eq_sym now gets its own eq_sym.u0, consistent
with eq_ind/eq_rect (whose generation already goes through the standard
case-analysis machinery) and with what a manually stated lemma gets.

Since the schemes of a family no longer share their universes,
hand-computed context sets would miss cross-scheme constraints (the
l2r rewriting scheme applies sym at the fresh universes, requiring
fresh <= sym.u0). Rather than computing those by hand, type-check the
built terms once with Typing.type_of and declare the resulting ustate.
Without this, the kernel rejection was silently swallowed by the
ignore_error in declare_rewriting_schemes, making eq_rew_r_dep vanish.

Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_019ttctspSoVoquHLQtbPVZw
(cherry picked from commit 2829830313bf14c7ee7c48bb108df73726e1f9af)
---
 .../22221-template-scheme-univs-Fixed.rst     | 13 ++++
 tactics/eqschemes.ml                          | 69 ++++++++++++++-----
 test-suite/bugs/bug_22220.v                   | 33 +++++++++
 3 files changed, 97 insertions(+), 18 deletions(-)
 create mode 100644 doc/changelog/11-corelib/22221-template-scheme-univs-Fixed.rst
 create mode 100644 test-suite/bugs/bug_22220.v

diff --git a/doc/changelog/11-corelib/22221-template-scheme-univs-Fixed.rst b/doc/changelog/11-corelib/22221-template-scheme-univs-Fixed.rst
new file mode 100644
index 000000000000..636a22f0deae
--- /dev/null
+++ b/doc/changelog/11-corelib/22221-template-scheme-univs-Fixed.rst
@@ -0,0 +1,13 @@
+- **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 <https://github.com/rocq-prover/rocq/pull/22221>`_,
+  fixes `#22220 <https://github.com/rocq-prover/rocq/issues/22220>`_,
+  by Jason Gross).
diff --git a/tactics/eqschemes.ml b/tactics/eqschemes.ml
index fadfbaa2f3c8..6282014d9b6e 100644
--- a/tactics/eqschemes.ml
+++ b/tactics/eqschemes.ml
@@ -84,6 +84,16 @@ let with_context_set ctx (b, ctx') =
 let of_context_set env ctx =
   UState.merge_sort_context_set ~sideff:false ~src:UState.Internal UnivRigid (UState.from_env env) ctx
 
+(* Type-check a hand-built scheme so as to collect the universe
+   constraints its context set does not explicitly contain, in
+   particular the constraints relating the fresh universes substituted
+   for template universes (see [maybe_template_instance]) to the
+   universes of the other schemes the term refers to. *)
+let retype_context_set env ctx c =
+  let sigma = Evd.from_ustate (of_context_set env ctx) in
+  let sigma, _ = Typing.type_of env sigma (EConstr.of_constr c) in
+  Evd.ustate sigma
+
 let build_dependent_inductive ind (mib,mip) =
   let realargs,_ = List.chop mip.mind_nrealdecls mip.mind_arity_ctxt in
   applist
@@ -91,11 +101,28 @@ let build_dependent_inductive ind (mib,mip) =
        Context.Rel.instance_list mkRel mip.mind_nrealdecls mib.mind_params_ctxt
        @ Context.Rel.instance_list mkRel 0 realargs)
 
+(* For a template polymorphic inductive, generate an instance to
+   substitute into the contexts copied from the inductive declaration.
+   Using the default template levels (e.g. eq.u0) would make the type of
+   the scheme mention global template universes, so that each use of the
+   scheme would in turn constrain them (see the bad-template-constraint
+   warning and #22220). We thus use fresh levels, which become universes
+   of the scheme; the accompanying context set must be declared by the
+   caller. Qualities are kept at their (all-QType) defaults since the
+   scheme is monomorphic. This instance is only used for substitution
+   into the copied contexts: occurrences of the inductive in the scheme
+   itself keep an empty instance, as required for template inductives. *)
 let maybe_template_instance (mib, mip) u = match mib.mind_template with
-| None -> u
+| None -> u, UnivGen.empty_sort_context
 | Some templ ->
   let () = assert (UVars.Instance.is_empty u) in
-  templ.template_defaults
+  let qdefaults, _ = UVars.Instance.to_array templ.template_defaults in
+  let _, ulen = UVars.AbstractContext.size templ.template_context in
+  let uinst = Array.init ulen (fun _ -> UnivGen.fresh_level ()) in
+  let inst = UVars.Instance.of_array (qdefaults, uinst) in
+  let us = Array.fold_right Univ.Level.Set.add uinst Univ.Level.Set.empty in
+  let csts = UVars.AbstractContext.instantiate inst templ.template_context in
+  inst, ((Sorts.QVar.Set.empty, us), csts)
 
 let named_hd env t na = named_hd env (Evd.from_env env) (EConstr.of_constr t) na
 let name_assumption env = function
@@ -145,7 +172,7 @@ let error msg = user_err Pp.(str msg)
 
 let get_sym_eq_data env (ind,u) =
   let (mib,mip as specif) = lookup_mind_specif env ind in
-  let u = maybe_template_instance specif u in
+  let u, ctx = maybe_template_instance specif u in
   if not (Int.equal (Array.length mib.mind_packets) 1) ||
     not (Int.equal (Array.length mip.mind_nf_lc) 1) then
     error "Not an inductive type with a single constructor.";
@@ -167,7 +194,7 @@ let get_sym_eq_data env (ind,u) =
   if not (List.equal Constr.equal params2 constrargs) then
     error "Constructors arguments must repeat the parameters.";
   (* nrealargs_ctxt and nrealargs are the same here *)
-  (specif,mip.mind_nrealargs,realsign,paramsctxt,paramsctxt1)
+  (specif,mip.mind_nrealargs,realsign,paramsctxt,paramsctxt1,ctx)
 
 (**********************************************************************)
 (* Check if an inductive type [ind] has the form                      *)
@@ -181,7 +208,7 @@ let get_sym_eq_data env (ind,u) =
 
 let get_non_sym_eq_data env (ind,u) =
   let (mib,mip as specif) = lookup_mind_specif env ind in
-  let u = maybe_template_instance specif u in
+  let u, ctx = maybe_template_instance specif u in
   if not (Int.equal (Array.length mib.mind_packets) 1) ||
     not (Int.equal (Array.length mip.mind_nf_lc) 1) then
     error "Not an inductive type with a single constructor.";
@@ -196,7 +223,7 @@ let get_non_sym_eq_data env (ind,u) =
   let _,constrargs = List.chop mib.mind_nparams constrargs in
   let constrargs = List.map (Vars.subst_instance_constr u) constrargs in
   let paramsctxt = Vars.subst_instance_context u mib.mind_params_ctxt in
-  (specif,constrargs,realsign,paramsctxt,mip.mind_nrealargs)
+  (specif,constrargs,realsign,paramsctxt,mip.mind_nrealargs,ctx)
 
 (**********************************************************************)
 (* Build the symmetry lemma associated to an inductive type           *)
@@ -214,8 +241,9 @@ let get_non_sym_eq_data env (ind,u) =
 
 let build_sym_scheme env _handle ind =
   let (ind,u as indu), ctx = UnivGen.fresh_inductive_instance env ind in
-  let (mib,mip as specif),nrealargs,realsign,paramsctxt,paramsctxt1 =
+  let (mib,mip as specif),nrealargs,realsign,paramsctxt,paramsctxt1,ctx' =
     get_sym_eq_data env indu in
+  let ctx = UnivGen.sort_context_union ctx ctx' in
   let cstr n =
     mkApp (mkConstructUi(indu,1),Context.Rel.instance mkRel n mib.mind_params_ctxt) in
   let varH,_ = fresh env (default_id_of_ind ind mip) Id.Set.empty in
@@ -245,7 +273,7 @@ let build_sym_scheme env _handle ind =
             mkRel 1 (* varH *),
             [|cstr (nrealargs+1)|])))))
   in
-  c, of_context_set env ctx
+  c, retype_context_set env ctx c
 
 let sym_scheme_kind =
   declare_individual_scheme_object "sym"
@@ -273,8 +301,9 @@ let const_of_scheme kind env handle ind ctx =
 
 let build_sym_involutive_scheme env handle ind =
   let (ind,u as indu), ctx = UnivGen.fresh_inductive_instance env ind in
-  let (mib,mip as specif),nrealargs,realsign,paramsctxt,paramsctxt1 =
+  let (mib,mip as specif),nrealargs,realsign,paramsctxt,paramsctxt1,ctx' =
     get_sym_eq_data env indu in
+  let ctx = UnivGen.sort_context_union ctx ctx' in
   let eq,eqrefl,ctx = get_rocq_eq env ctx in
   let sym, ctx = const_of_scheme sym_scheme_kind env handle ind ctx in
   let cstr n = mkApp (mkConstructUi (indu,1),Context.Rel.instance mkRel n paramsctxt) in
@@ -315,7 +344,7 @@ let build_sym_involutive_scheme env handle ind =
                NoInvert,
                mkRel 1 (* varH *),
                [|mkApp(eqrefl,[|applied_ind_C;cstr (nrealargs+1)|])|])))))
-  in (c, of_context_set env ctx)
+  in (c, retype_context_set env ctx c)
 
 let sym_involutive_scheme_kind =
   declare_individual_scheme_object "sym_involutive"
@@ -384,8 +413,9 @@ let sym_involutive_scheme_kind =
 
 let build_l2r_rew_scheme dep env handle ind kind =
   let (ind,u as indu), ctx = UnivGen.fresh_inductive_instance env ind in
-  let (mib,mip as specif),nrealargs,realsign,paramsctxt,paramsctxt1 =
+  let (mib,mip as specif),nrealargs,realsign,paramsctxt,paramsctxt1,ctx' =
     get_sym_eq_data env indu in
+  let ctx = UnivGen.sort_context_union ctx ctx' in
   let sym, ctx = const_of_scheme sym_scheme_kind env handle ind ctx in
   let sym_involutive, ctx = const_of_scheme sym_involutive_scheme_kind env handle ind ctx in
   let eq,eqrefl,ctx = get_rocq_eq env ctx in
@@ -474,7 +504,7 @@ let build_l2r_rew_scheme dep env handle ind kind =
        [|main_body|]))
    else
      main_body))))))
-  in (c, of_context_set env ctx)
+  in (c, retype_context_set env ctx c)
 
 (**********************************************************************)
 (* Build the left-to-right rewriting lemma for hypotheses associated  *)
@@ -504,8 +534,9 @@ let build_l2r_rew_scheme dep env handle ind kind =
 
 let build_l2r_forward_rew_scheme dep env ind kind =
   let (ind,u as indu), ctx = UnivGen.fresh_inductive_instance env ind in
-  let (mib,mip as specif),nrealargs,realsign,paramsctxt,paramsctxt1 =
+  let (mib,mip as specif),nrealargs,realsign,paramsctxt,paramsctxt1,ctx' =
     get_sym_eq_data env indu in
+  let ctx = UnivGen.sort_context_union ctx ctx' in
   let cstr n p =
     mkApp (mkConstructUi(indu,1),
       Array.concat [Context.Rel.instance mkRel n paramsctxt1;
@@ -566,7 +597,7 @@ let build_l2r_forward_rew_scheme dep env ind kind =
           (if dep then realsign_ind_P 1 applied_ind_P' else realsign_P 2) s)
       (mkNamedLambda (make_annot varHC sr) applied_PC'
         (mkVar varHC))|]))))))
-  in c, of_context_set env ctx
+  in c, retype_context_set env ctx c
 
 (**********************************************************************)
 (* Build the right-to-left rewriting lemma for hypotheses associated  *)
@@ -600,8 +631,9 @@ let build_l2r_forward_rew_scheme dep env ind kind =
 
 let build_r2l_forward_rew_scheme dep env ind kind =
   let (ind,u as indu), ctx = UnivGen.fresh_inductive_instance env ind in
-  let ((mib,mip as specif),constrargs,realsign,paramsctxt,nrealargs) =
+  let ((mib,mip as specif),constrargs,realsign,paramsctxt,nrealargs,ctx') =
     get_non_sym_eq_data env indu in
+  let ctx = UnivGen.sort_context_union ctx ctx' in
   let cstr n =
     mkApp (mkConstructUi(indu,1),Context.Rel.instance mkRel n mib.mind_params_ctxt) in
   let constrargs_cstr = constrargs@[cstr 0] in
@@ -652,7 +684,7 @@ let build_r2l_forward_rew_scheme dep env ind kind =
            lift (nrealargs+3) applied_PC,
            mkRel 1)|])),
     [|mkVar varHC|]))))))
-  in c, of_context_set env ctx
+  in c, retype_context_set env ctx c
 
 (**********************************************************************)
 (* This function "repairs" the non-dependent r2l forward rewriting    *)
@@ -810,7 +842,8 @@ let build_congr env (eq,refl,ctx) ind =
   let (ind,u as indu), ctx = with_context_set ctx
     (UnivGen.fresh_inductive_instance env ind) in
   let (mib,mip) = lookup_mind_specif env ind in
-  let u = maybe_template_instance (mib, mip) u in
+  let u, ctx' = maybe_template_instance (mib, mip) u in
+  let ctx = UnivGen.sort_context_union ctx ctx' in
   if not (Int.equal (Array.length mib.mind_packets) 1) || not (Int.equal (Array.length mip.mind_nf_lc) 1) then
     error "Not an inductive type with a single constructor.";
   if not (Int.equal mip.mind_nrealargs 1) then
@@ -871,7 +904,7 @@ let build_congr env (eq,refl,ctx) ind =
        [|mkApp (refl,
           [|mkVar varB;
             mkApp (mkVar varf, [|lift (mip.mind_nrealargs+3) b|])|])|])))))))
-  in c, of_context_set env ctx
+  in c, retype_context_set env ctx c
 
 let congr_scheme_kind = declare_individual_scheme_object "congr"
   (fun env _ ind ->
diff --git a/test-suite/bugs/bug_22220.v b/test-suite/bugs/bug_22220.v
new file mode 100644
index 000000000000..c1300895e74a
--- /dev/null
+++ b/test-suite/bugs/bug_22220.v
@@ -0,0 +1,33 @@
+(* Schemes over template polymorphic inductives (Scheme Rewriting) should
+   not mention the global template universes in their types, so that using
+   them does not constrain the template universes.
+   See https://github.com/rocq-prover/rocq/issues/22220 *)
+Set Warnings "+bad-template-constraint".
+
+(* Eta-expansion constrains the universe of the first argument; this must
+   not touch eq.u0. *)
+Check (fun x => @eq_sym x).
+Check (fun x => @eq_sym_involutive x).
+Check (fun x => @eq_rew x).
+Check (fun x => @eq_rew_dep x).
+Check (fun x => @eq_rew_fwd_dep x).
+Check (fun x => @eq_rew_r x).
+Check (fun x => @eq_rew_r_dep x).
+Check (fun x => @eq_rew_fwd_r_dep x).
+
+(* These were already fine and must stay so. *)
+Check (fun x => @eq_ind x).
+Check (fun x => @eq_rect x).
+Check (fun x => @eq_trans x).
+Check (fun x => @f_equal x).
+
+(* The schemes must still be usable at arbitrary universes. *)
+Goal forall (A : Type) (x y : A), x = y -> y = x.
+Proof. intros A x y H. exact (eq_sym H). Qed.
+
+(* Scheme generation itself must also work with the warning as error. *)
+Inductive myeq (A:Type) (x:A) : A -> Prop := myeq_refl : myeq A x x.
+Scheme Rewriting for myeq.
+Check (fun x => @myeq_sym x).
+Check (fun x => @myeq_sym_involutive x).
+Check (fun x => @myeq_rew_r_dep x).

From 204877933be689bf2c741a8fbc3408604f995c05 Mon Sep 17 00:00:00 2001
From: Jason Gross <jason@theorem.dev>
Date: Tue, 7 Jul 2026 18:00:20 +0000
Subject: [PATCH 15/28] Compute cross-scheme universe constraints explicitly

Address review: instead of re-typechecking the hand-built schemes with
Typing.type_of to recover the universe constraints missing from the
hand-computed context sets, compute them explicitly.  Since the
schemes of an inductive type no longer share the universes standing
for its template universes, the builders that apply a previously
declared scheme (sym_involutive and l2r_rew, via const_of_scheme) must
enforce the sorts of the parameters of the scheme being built to fit
in the sorts of the corresponding binders of the applied constant,
e.g. eq_rew_r_dep.u0 <= eq_sym.u0.  These constraints were previously
invisible because all schemes shared the default template levels
(eq.u0 <= eq.u0).  The other builders' context sets are
self-contained: in particular, applications of template inductives
(the inductive itself, and eq) need no constraints since the kernel
instantiates them at application time; bugs/bug_22220.v now also
tests this with a Type-sorted equality.

Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_019ttctspSoVoquHLQtbPVZw
(cherry picked from commit c93c0b424a208da7a9b27eebcb26b7cf34924208)
---
 tactics/eqschemes.ml        | 70 +++++++++++++++++++++++++------------
 test-suite/bugs/bug_22220.v |  9 +++++
 2 files changed, 57 insertions(+), 22 deletions(-)

diff --git a/tactics/eqschemes.ml b/tactics/eqschemes.ml
index 6282014d9b6e..f6df05e3cc9d 100644
--- a/tactics/eqschemes.ml
+++ b/tactics/eqschemes.ml
@@ -84,16 +84,6 @@ let with_context_set ctx (b, ctx') =
 let of_context_set env ctx =
   UState.merge_sort_context_set ~sideff:false ~src:UState.Internal UnivRigid (UState.from_env env) ctx
 
-(* Type-check a hand-built scheme so as to collect the universe
-   constraints its context set does not explicitly contain, in
-   particular the constraints relating the fresh universes substituted
-   for template universes (see [maybe_template_instance]) to the
-   universes of the other schemes the term refers to. *)
-let retype_context_set env ctx c =
-  let sigma = Evd.from_ustate (of_context_set env ctx) in
-  let sigma, _ = Typing.type_of env sigma (EConstr.of_constr c) in
-  Evd.ustate sigma
-
 let build_dependent_inductive ind (mib,mip) =
   let realargs,_ = List.chop mip.mind_nrealdecls mip.mind_arity_ctxt in
   applist
@@ -111,7 +101,11 @@ let build_dependent_inductive ind (mib,mip) =
    caller. Qualities are kept at their (all-QType) defaults since the
    scheme is monomorphic. This instance is only used for substitution
    into the copied contexts: occurrences of the inductive in the scheme
-   itself keep an empty instance, as required for template inductives. *)
+   itself keep an empty instance, as required for template inductives.
+   Since the schemes of an inductive type no longer share universes, a
+   scheme applying a previously declared scheme also needs constraints
+   relating its universes to those of the latter (see
+   [enforce_scheme_param_univs]). *)
 let maybe_template_instance (mib, mip) u = match mib.mind_template with
 | None -> u, UnivGen.empty_sort_context
 | Some templ ->
@@ -273,7 +267,7 @@ let build_sym_scheme env _handle ind =
             mkRel 1 (* varH *),
             [|cstr (nrealargs+1)|])))))
   in
-  c, retype_context_set env ctx c
+  c, of_context_set env ctx
 
 let sym_scheme_kind =
   declare_individual_scheme_object "sym"
@@ -295,9 +289,41 @@ let sym_scheme_kind =
 (*                                                                    *)
 (**********************************************************************)
 
-let const_of_scheme kind env handle ind ctx =
+(* The universes standing for the template universes of the inductive
+   type are local to each scheme (see [maybe_template_instance]), so
+   the parameters of two schemes of the same inductive type live at a
+   priori unrelated universes. Applying the constant [c] of a
+   previously declared scheme to the parameters of the scheme being
+   built thus requires the sorts of the parameters of the latter to fit
+   in the sorts of the corresponding binders of the type of [c]. The
+   two parameter contexts have the same shape, except that the let-ins
+   of [paramsctxt] do not appear in the kernel-inferred type of [c]. *)
+let enforce_scheme_param_univs env paramsctxt c ctx =
+  let univ_of_param t =
+    let _, s = decompose_prod_decls t in
+    if isSort s then Some (Sorts.univ_of_sort (destSort s)) else None
+  in
+  let rec fold ctx params t = match params with
+  | [] -> ctx
+  | LocalDef _ :: params -> fold ctx params t
+  | LocalAssum (_, ty) :: params ->
+    let _, cty, t = destProd t in
+    let ctx = match univ_of_param ty, univ_of_param cty with
+    | Some u, Some cu ->
+      (* trivial constraints, i.e. between global universes shared by
+         the two schemes, are dropped by enforce_leq *)
+      let qus, (qcst, ucst) = ctx in
+      qus, (qcst, UnivSubst.enforce_leq u cu ucst)
+    | _ -> ctx
+    in
+    fold ctx params t
+  in
+  fold ctx (List.rev paramsctxt) (Typeops.type_of_constant_in env (destConst c))
+
+let const_of_scheme kind env handle ind paramsctxt ctx =
   let sym_scheme = match local_lookup_scheme handle kind ind with Some cst -> cst | None -> assert false in
-  with_context_set ctx (UnivGen.fresh_global_instance env sym_scheme)
+  let c, ctx = with_context_set ctx (UnivGen.fresh_global_instance env sym_scheme) in
+  c, enforce_scheme_param_univs env paramsctxt c ctx
 
 let build_sym_involutive_scheme env handle ind =
   let (ind,u as indu), ctx = UnivGen.fresh_inductive_instance env ind in
@@ -305,7 +331,7 @@ let build_sym_involutive_scheme env handle ind =
     get_sym_eq_data env indu in
   let ctx = UnivGen.sort_context_union ctx ctx' in
   let eq,eqrefl,ctx = get_rocq_eq env ctx in
-  let sym, ctx = const_of_scheme sym_scheme_kind env handle ind ctx in
+  let sym, ctx = const_of_scheme sym_scheme_kind env handle ind paramsctxt ctx in
   let cstr n = mkApp (mkConstructUi (indu,1),Context.Rel.instance mkRel n paramsctxt) in
   let indr = UVars.subst_instance_relevance u mip.mind_relevance in
   let varH,_ = fresh env (default_id_of_ind ind mip) Id.Set.empty in
@@ -344,7 +370,7 @@ let build_sym_involutive_scheme env handle ind =
                NoInvert,
                mkRel 1 (* varH *),
                [|mkApp(eqrefl,[|applied_ind_C;cstr (nrealargs+1)|])|])))))
-  in (c, retype_context_set env ctx c)
+  in (c, of_context_set env ctx)
 
 let sym_involutive_scheme_kind =
   declare_individual_scheme_object "sym_involutive"
@@ -416,8 +442,8 @@ let build_l2r_rew_scheme dep env handle ind kind =
   let (mib,mip as specif),nrealargs,realsign,paramsctxt,paramsctxt1,ctx' =
     get_sym_eq_data env indu in
   let ctx = UnivGen.sort_context_union ctx ctx' in
-  let sym, ctx = const_of_scheme sym_scheme_kind env handle ind ctx in
-  let sym_involutive, ctx = const_of_scheme sym_involutive_scheme_kind env handle ind ctx in
+  let sym, ctx = const_of_scheme sym_scheme_kind env handle ind paramsctxt ctx in
+  let sym_involutive, ctx = const_of_scheme sym_involutive_scheme_kind env handle ind paramsctxt ctx in
   let eq,eqrefl,ctx = get_rocq_eq env ctx in
   let cstr n p =
     mkApp (mkConstructUi(indu,1),
@@ -504,7 +530,7 @@ let build_l2r_rew_scheme dep env handle ind kind =
        [|main_body|]))
    else
      main_body))))))
-  in (c, retype_context_set env ctx c)
+  in (c, of_context_set env ctx)
 
 (**********************************************************************)
 (* Build the left-to-right rewriting lemma for hypotheses associated  *)
@@ -597,7 +623,7 @@ let build_l2r_forward_rew_scheme dep env ind kind =
           (if dep then realsign_ind_P 1 applied_ind_P' else realsign_P 2) s)
       (mkNamedLambda (make_annot varHC sr) applied_PC'
         (mkVar varHC))|]))))))
-  in c, retype_context_set env ctx c
+  in c, of_context_set env ctx
 
 (**********************************************************************)
 (* Build the right-to-left rewriting lemma for hypotheses associated  *)
@@ -684,7 +710,7 @@ let build_r2l_forward_rew_scheme dep env ind kind =
            lift (nrealargs+3) applied_PC,
            mkRel 1)|])),
     [|mkVar varHC|]))))))
-  in c, retype_context_set env ctx c
+  in c, of_context_set env ctx
 
 (**********************************************************************)
 (* This function "repairs" the non-dependent r2l forward rewriting    *)
@@ -904,7 +930,7 @@ let build_congr env (eq,refl,ctx) ind =
        [|mkApp (refl,
           [|mkVar varB;
             mkApp (mkVar varf, [|lift (mip.mind_nrealargs+3) b|])|])|])))))))
-  in c, retype_context_set env ctx c
+  in c, of_context_set env ctx
 
 let congr_scheme_kind = declare_individual_scheme_object "congr"
   (fun env _ ind ->
diff --git a/test-suite/bugs/bug_22220.v b/test-suite/bugs/bug_22220.v
index c1300895e74a..d617f6b83721 100644
--- a/test-suite/bugs/bug_22220.v
+++ b/test-suite/bugs/bug_22220.v
@@ -31,3 +31,12 @@ Scheme Rewriting for myeq.
 Check (fun x => @myeq_sym x).
 Check (fun x => @myeq_sym_involutive x).
 Check (fun x => @myeq_rew_r_dep x).
+
+(* Also for a Type-sorted equality: the uses of eq applied to a
+   Type-sorted inductive in the sym_involutive and rew_r_dep schemes
+   must not constrain eq.u0 either. *)
+Inductive myeqT (A:Type) (x:A) : A -> Type := myeqT_refl : myeqT A x x.
+Scheme Rewriting for myeqT.
+Check (fun x => @myeqT_sym x).
+Check (fun x => @myeqT_sym_involutive x).
+Check (fun x => @myeqT_rew_r_dep x).

From cb083265aba23e08954195e4eabd638ddaec2848 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Ga=C3=ABtan=20Gilbert?= <gaetan.gilbert@skyskimmer.net>
Date: Wed, 8 Jul 2026 13:09:58 +0200
Subject: [PATCH 16/28] Delete unused regexes in rocqdep lexer

(cherry picked from commit 2eac902cb6f6e0ccd39326ceb097c84fcadbc336)
---
 tools/coqdep/lib/lexer.mll | 6 ------
 1 file changed, 6 deletions(-)

diff --git a/tools/coqdep/lib/lexer.mll b/tools/coqdep/lib/lexer.mll
index 38b37428437b..22419dadf392 100644
--- a/tools/coqdep/lib/lexer.mll
+++ b/tools/coqdep/lib/lexer.mll
@@ -76,16 +76,10 @@
 }
 
 let space = [' ' '\t' '\n' '\r']
-let lowercase = ['a'-'z']
-let uppercase = ['A'-'Z']
-let identchar = ['A'-'Z' 'a'-'z' '_' '\'' '0'-'9']
-let caml_up_ident = uppercase identchar*
-let caml_low_ident = lowercase identchar*
 
 (* This is an overapproximation, we check correctness afterwards *)
 let coq_ident = ['A'-'Z' 'a'-'z' '_' '\128'-'\255'] ['A'-'Z' 'a'-'z' '_' '\'' '0'-'9' '\128'-'\255']*
 let coq_field = '.' coq_ident
-let coq_qual_id_rex = coq_ident coq_field+
 
 let dot = '.' ( space+ | eof)
 

From 6cc93ab71cb900625818c9145a8ee71ad418b641 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Ga=C3=ABtan=20Gilbert?= <gaetan.gilbert@skyskimmer.net>
Date: Wed, 8 Jul 2026 13:35:00 +0200
Subject: [PATCH 17/28] rocqdep get location info directly instead of reparsing

The "_pos" fields are accurate even when running with positions disabled.

(cherry picked from commit 970c226f722aa2cff6232d8f441d41d3d186c7b3)
---
 tools/coqdep/lib/common.ml | 36 +++---------------------------------
 tools/coqdep/lib/lexer.mll |  4 +++-
 2 files changed, 6 insertions(+), 34 deletions(-)

diff --git a/tools/coqdep/lib/common.ml b/tools/coqdep/lib/common.ml
index dcbab8d983a2..b2bbb5a80117 100644
--- a/tools/coqdep/lib/common.ml
+++ b/tools/coqdep/lib/common.ml
@@ -152,12 +152,6 @@ let coq_to_stdlib from strl =
   | Some from -> Some (tr_qualid from), strl
   | None -> None, List.map tr_qualid strl
 
-let with_in_channel ~fname f =
-  let chan = try open_in fname
-    with Sys_error msg -> Error.cannot_open fname msg
-  in
-  Util.try_finally f chan close_in chan
-
 let with_in_descr ~fname f =
   let descr =
     try Unix.openfile fname [O_RDONLY] 0o000
@@ -177,8 +171,6 @@ module State = struct
   let loadpath x = x.loadpath
 end
 
-exception SyntaxErrorInFile of string
-
 (* recursive because of Load *)
 let rec find_dependencies ({State.vAccu; separator_hack; loadpath} as st) basename =
   (* Visited marks *)
@@ -203,19 +195,16 @@ let rec find_dependencies ({State.vAccu; separator_hack; loadpath} as st) basena
   let f = basename ^ ".v" in
   with_in_descr ~fname:f @@ fun chan ->
   (* For lexing efficiency purposes, we ignore the positions in this function.
-     This will force us to reparse the file in case of error to get a proper
-     location, but in practice such errors should be exceedingly rare with
-     rocqdep. This lexer is indeed basically able to handle random nonsense
-     thrown at it. *)
+     We can still get accurate character counts, we're just missing newline info. *)
   let buf = lexbuf_from_descr ~with_positions:false chan in
   let open Lexer in
   let rec loop () =
     match coq_action buf with
     | exception Fin_fichier ->
       DepSet.elements !dependencies
-    | exception Syntax_error _ ->
+    | exception Syntax_error (i,j) ->
       (* The locations are garbage due to with_positions:false, ignore them *)
-      raise (SyntaxErrorInFile f)
+      Error.cannot_parse f (i, j)
     | tok ->  match tok with
       | Require (from, strl) ->
         let from, strl = coq_to_stdlib from strl in
@@ -288,25 +277,6 @@ let rec find_dependencies ({State.vAccu; separator_hack; loadpath} as st) basena
   in
   loop ()
 
-(* Reparse the file to get the error location *)
-let get_parse_error f =
-  with_in_channel ~fname:f @@ fun chan ->
-  let buf = Lexing.from_channel chan in
-  let rec loop () = match Lexer.coq_action buf with
-  | _tok -> loop ()
-  | exception Lexer.Syntax_error (i, j) -> (i, j)
-  | exception Lexer.Fin_fichier ->
-    (* may technically happen due to race conditions, return a dummy value *)
-    (0, 0)
-  in
-  loop ()
-
-let find_dependencies st basename =
-  try find_dependencies st basename
-  with SyntaxErrorInFile f ->
-    let (i, j) = get_parse_error f in
-    Error.cannot_parse f (i, j)
-
 let compute_deps st =
   let mk_dep name = Dep_info.make ~name ~deps:(find_dependencies st name) in
   List.rev st.vAccu.acc |> List.to_seq |> Seq.map mk_dep
diff --git a/tools/coqdep/lib/lexer.mll b/tools/coqdep/lib/lexer.mll
index 22419dadf392..6e2a09703a9a 100644
--- a/tools/coqdep/lib/lexer.mll
+++ b/tools/coqdep/lib/lexer.mll
@@ -37,7 +37,9 @@
     lexbuf.lex_curr_p <- lexbuf.lex_start_p
 
   let syntax_error lexbuf =
-    raise (Syntax_error (Lexing.lexeme_start lexbuf, Lexing.lexeme_end lexbuf))
+    (* abs_pos is position of the start of the buffer in the file
+       start/curr_pos are positions in the buffer *)
+    raise (Syntax_error (lexbuf.lex_abs_pos + lexbuf.lex_start_pos, lexbuf.lex_abs_pos + lexbuf.lex_curr_pos))
 
   let check_valid lexbuf s =
     match Unicode.ident_refutation s with

From 694905a0773d3a2e72e2ff1e6d14ce326cd0cd79 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Ga=C3=ABtan=20Gilbert?= <gaetan.gilbert@skyskimmer.net>
Date: Wed, 8 Jul 2026 13:36:44 +0200
Subject: [PATCH 18/28] Use Loc.t for syntax error locations in rocqdep

This requires rereading the file to get line number counts.

(cherry picked from commit 9ae02585998ea3252c8edfaaed4fe33eb506d12a)
---
 tools/coqdep/lib/common.ml       | 23 ++++++++++++++++++++++-
 tools/coqdep/lib/error.ml        |  9 ++++-----
 tools/coqdep/lib/error.mli       |  7 +------
 tools/coqdep/lib/rocqdep_main.ml |  4 +++-
 4 files changed, 30 insertions(+), 13 deletions(-)

diff --git a/tools/coqdep/lib/common.ml b/tools/coqdep/lib/common.ml
index b2bbb5a80117..b639c260442a 100644
--- a/tools/coqdep/lib/common.ml
+++ b/tools/coqdep/lib/common.ml
@@ -8,6 +8,27 @@
 (*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
+(* count newlines to get a nice error location instead of raw chars *)
+let get_loc f start end_ =
+  let ch = open_in f in
+  let rec loop lnum bol read =
+    if read = start then lnum, bol
+    else match input_char ch with
+      | '\n' -> loop (lnum+1) (read+1) (read+1)
+      | _ -> loop lnum bol (read+1)
+  in
+  let lnum, bol = loop 1 0 0 in
+  { Loc.fname = InFile { dirpath=None; file=f };
+    line_nb = lnum;
+    bol_pos = bol;
+    bp = start;
+    ep = end_;
+
+    (* not used by printing *)
+    line_nb_last = 0;
+    bol_pos_last = 0;
+  }
+
 (** Rocq files specifies on the command line:
     - first string is the full filename, with only its extension removed
     - second string is the absolute version of the previous (via getcwd)
@@ -204,7 +225,7 @@ let rec find_dependencies ({State.vAccu; separator_hack; loadpath} as st) basena
       DepSet.elements !dependencies
     | exception Syntax_error (i,j) ->
       (* The locations are garbage due to with_positions:false, ignore them *)
-      Error.cannot_parse f (i, j)
+      Error.cannot_parse ~loc:(get_loc f i j)
     | tok ->  match tok with
       | Require (from, strl) ->
         let from, strl = coq_to_stdlib from strl in
diff --git a/tools/coqdep/lib/error.ml b/tools/coqdep/lib/error.ml
index 8f3c544be50d..f8e2fa10c61c 100644
--- a/tools/coqdep/lib/error.ml
+++ b/tools/coqdep/lib/error.ml
@@ -8,7 +8,7 @@
 (*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
-exception CannotParseFile of string * (int * int)
+exception CannotParseFile
 exception CannotParseProjectFile of string * string
 
 exception CannotOpenFile of string * string
@@ -16,9 +16,8 @@ exception CannotOpenProjectFile of string
 
 
 let () = CErrors.register_handler @@ function
-  | CannotParseFile (s,(i,j)) ->
-    Some Pp.(str "File \"" ++ str s ++ str "\"," ++ str "characters" ++ spc ()
-      ++ int i ++ str "-" ++ int j ++ str ":" ++ spc () ++ str "Syntax error")
+  | CannotParseFile ->
+    Some Pp.(str "Syntax error")
 
   | CannotParseProjectFile (file, msg) ->
     Some Pp.(str "Project file" ++ spc () ++ str  "\"" ++ str file ++ str "\":" ++ spc ()
@@ -33,7 +32,7 @@ let () = CErrors.register_handler @@ function
 
   | _ -> None
 
-let cannot_parse s ij = raise @@ CannotParseFile (s, ij)
+let cannot_parse ~loc = Loc.raise ~loc @@ CannotParseFile
 let cannot_open_project_file msg = raise @@ CannotOpenProjectFile msg
 let cannot_parse_project_file file msg = raise @@ CannotParseProjectFile (file, msg)
 let cannot_open s msg = raise @@ CannotOpenFile (s, msg)
diff --git a/tools/coqdep/lib/error.mli b/tools/coqdep/lib/error.mli
index 2cee33dd053c..3db02f928e56 100644
--- a/tools/coqdep/lib/error.mli
+++ b/tools/coqdep/lib/error.mli
@@ -8,12 +8,7 @@
 (*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
-exception CannotParseFile of string * (int * int)
-exception CannotParseProjectFile of string * string
-exception CannotOpenFile of string * string
-exception CannotOpenProjectFile of string
-
-val cannot_parse : string -> int * int -> 'a
+val cannot_parse : loc:Loc.t -> 'a
 val cannot_open_project_file : string -> 'a
 val cannot_parse_project_file : string -> string -> 'a
 val cannot_open : string -> string -> 'a
diff --git a/tools/coqdep/lib/rocqdep_main.ml b/tools/coqdep/lib/rocqdep_main.ml
index 4f2c04a698e1..6282aa3c9daa 100644
--- a/tools/coqdep/lib/rocqdep_main.ml
+++ b/tools/coqdep/lib/rocqdep_main.ml
@@ -56,5 +56,7 @@ let main args =
   try
     coqdep args
   with exn ->
-    Format.eprintf "*** Error: @[%a@]@\n%!" Pp.pp_with (CErrors.print exn);
+    let exn = Exninfo.capture exn in
+    let loc = Loc.get_loc (snd exn) in
+    Feedback.msg_notice ?loc Pp.(str "Error: " ++ CErrors.iprint exn);
     exit 1

From a1d09230b8f74e7e5f1071b6483577e52f7d80fd Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Ga=C3=ABtan=20Gilbert?= <gaetan.gilbert@skyskimmer.net>
Date: Wed, 8 Jul 2026 13:54:45 +0200
Subject: [PATCH 19/28] rocqdep print location for module not found warning

Fix #10815

(cherry picked from commit a25317a8ae623a93b847be434db821981d1a7768)
---
 lib/feedback.ml                               | 10 ++----
 .../misc/coqdep-require-filter-categories.sh  |  4 +--
 .../coqdep-require-filter-categories/fA.v     |  3 +-
 .../stderr.ref                                |  3 +-
 .../misc/external-deps/file1.notfound.deps    |  3 +-
 test-suite/misc/external-deps/file1.v         |  3 +-
 .../misc/external-deps/file2.notfound.deps    |  3 +-
 tools/coqdep/lib/common.ml                    | 21 ++++++-----
 tools/coqdep/lib/lexer.mli                    |  8 +++--
 tools/coqdep/lib/lexer.mll                    | 35 +++++++++++++------
 tools/dune_rule_gen/gen_rules.ml              |  7 +---
 11 files changed, 56 insertions(+), 44 deletions(-)

diff --git a/lib/feedback.ml b/lib/feedback.ml
index 9823a2c8a415..0ace8e857699 100644
--- a/lib/feedback.ml
+++ b/lib/feedback.ml
@@ -102,13 +102,9 @@ let msg_debug   ?loc x = feedback_logger ?loc Debug x
 (* Helper for tools willing to understand only the messages *)
 let console_feedback_listener fmt =
   let open Format in
-  let pp_loc fmt loc = let open Loc in match loc with
-    | None     -> fprintf fmt ""
-    | Some loc ->
-      let where =
-        match loc.fname with InFile { file } -> file | ToplevelInput -> "Toplevel input" in
-      fprintf fmt "\"%s\", line %d, characters %d-%d:@\n"
-        where loc.line_nb (loc.bp-loc.bol_pos) (loc.ep-loc.bol_pos) in
+  let pp_loc fmt = function
+    | None     -> ()
+    | Some loc -> Pp.pp_with fmt Pp.(Loc.pr loc ++ str ":" ++ fnl()) in
   let checker_feed (fb : feedback) =
   match fb.contents with
   | Processed   -> ()
diff --git a/test-suite/misc/coqdep-require-filter-categories.sh b/test-suite/misc/coqdep-require-filter-categories.sh
index 6866752fd47e..4ca500b9fd3f 100755
--- a/test-suite/misc/coqdep-require-filter-categories.sh
+++ b/test-suite/misc/coqdep-require-filter-categories.sh
@@ -7,7 +7,7 @@ cd misc/coqdep-require-filter-categories
 code=0
 $coqdep -worker @ROCQWORKER@ -R . 'Bla' ./*.v > stdout 2> stderr || code=$?
 
-diff stdout.ref stdout
-diff stderr.ref stderr
+diff -u stdout.ref stdout
+diff -u stderr.ref stderr
 
 exit $code
diff --git a/test-suite/misc/coqdep-require-filter-categories/fA.v b/test-suite/misc/coqdep-require-filter-categories/fA.v
index cf54686cbfd9..b025b403e296 100644
--- a/test-suite/misc/coqdep-require-filter-categories/fA.v
+++ b/test-suite/misc/coqdep-require-filter-categories/fA.v
@@ -1 +1,2 @@
-Require Import Prelude(something(..)) nonexistent.
+(* a
+ comment *) Require Import Prelude(something(..)) nonexistent.
diff --git a/test-suite/misc/coqdep-require-filter-categories/stderr.ref b/test-suite/misc/coqdep-require-filter-categories/stderr.ref
index c83fb7a445a5..0b19339d1271 100644
--- a/test-suite/misc/coqdep-require-filter-categories/stderr.ref
+++ b/test-suite/misc/coqdep-require-filter-categories/stderr.ref
@@ -1,3 +1,4 @@
-Warning: in file fA.v, library
+File "fA.v", line 2, characters 50-61:
+Warning: library
          nonexistent is required and has not been found in the loadpath!
          [module-not-found,filesystem,default]
diff --git a/test-suite/misc/external-deps/file1.notfound.deps b/test-suite/misc/external-deps/file1.notfound.deps
index 2b3d7ab40db0..56c16d6f5183 100644
--- a/test-suite/misc/external-deps/file1.notfound.deps
+++ b/test-suite/misc/external-deps/file1.notfound.deps
@@ -1,4 +1,5 @@
-Warning: in file misc/external-deps/file1.v, external file d1 is required
+File "misc/external-deps/file1.v", line 2, characters 51-55:
+Warning: external file d1 is required
          from root foo.bar and has not been found in the loadpath!
          [module-not-found,filesystem,default]
 misc/external-deps/file1.vo misc/external-deps/file1.glob misc/external-deps/file1.v.beautified misc/external-deps/file1.required_vo: misc/external-deps/file1.v @ROCQWORKER@
diff --git a/test-suite/misc/external-deps/file1.v b/test-suite/misc/external-deps/file1.v
index 1e331d0723ab..c061121b6206 100644
--- a/test-suite/misc/external-deps/file1.v
+++ b/test-suite/misc/external-deps/file1.v
@@ -1 +1,2 @@
-Comments From foo.bar Extra Dependency "d1".
+(* a
+ comment *) Comments From foo.bar Extra Dependency "d1".
diff --git a/test-suite/misc/external-deps/file2.notfound.deps b/test-suite/misc/external-deps/file2.notfound.deps
index 90cf56ec4a78..3b7fc1f7976e 100644
--- a/test-suite/misc/external-deps/file2.notfound.deps
+++ b/test-suite/misc/external-deps/file2.notfound.deps
@@ -1,4 +1,5 @@
-Warning: in file misc/external-deps/file2.v, external file d1 is required
+File "misc/external-deps/file2.v", line 1, characters 30-34:
+Warning: external file d1 is required
          from root foo.bar and has not been found in the loadpath!
          [module-not-found,filesystem,default]
 misc/external-deps/file2.vo misc/external-deps/file2.glob misc/external-deps/file2.v.beautified misc/external-deps/file2.required_vo: misc/external-deps/file2.v @ROCQWORKER@
diff --git a/tools/coqdep/lib/common.ml b/tools/coqdep/lib/common.ml
index b639c260442a..dc57ea4faa4e 100644
--- a/tools/coqdep/lib/common.ml
+++ b/tools/coqdep/lib/common.ml
@@ -9,7 +9,7 @@
 (************************************************************************)
 
 (* count newlines to get a nice error location instead of raw chars *)
-let get_loc f start end_ =
+let get_loc f { Lexer.loc_start = start; loc_end = end_ } =
   let ch = open_in f in
   let rec loop lnum bol read =
     if read = start then lnum, bol
@@ -66,9 +66,8 @@ type what = Library | External
 let str_of_what = function Library -> "library" | External -> "external file"
 
 let warning_module_notfound =
-  let warn (what, from, f, s) =
+  let warn (what, from, s) =
     let open Pp in
-    str "in file " ++ str f ++ str ", " ++
     str (str_of_what what) ++ spc () ++ str (String.concat "." s) ++ str " is required" ++
     pr_opt (fun pth -> str "from root " ++ str (String.concat "." pth)) from ++
     str " and has not been found in the loadpath!"
@@ -171,7 +170,7 @@ let coq_to_stdlib from strl =
     | l -> l in
   match from with
   | Some from -> Some (tr_qualid from), strl
-  | None -> None, List.map tr_qualid strl
+  | None -> None, List.map (Util.on_snd tr_qualid) strl
 
 let with_in_descr ~fname f =
   let descr =
@@ -223,13 +222,13 @@ let rec find_dependencies ({State.vAccu; separator_hack; loadpath} as st) basena
     match coq_action buf with
     | exception Fin_fichier ->
       DepSet.elements !dependencies
-    | exception Syntax_error (i,j) ->
+    | exception Syntax_error loc ->
       (* The locations are garbage due to with_positions:false, ignore them *)
-      Error.cannot_parse ~loc:(get_loc f i j)
+      Error.cannot_parse ~loc:(get_loc f loc)
     | tok ->  match tok with
       | Require (from, strl) ->
         let from, strl = coq_to_stdlib from strl in
-        let decl str =
+        let decl (loc, str) =
           if should_visit_v_and_mark from str then begin
             let files = safe_assoc loadpath from f str in
             let files = match from, files with
@@ -242,7 +241,7 @@ let rec find_dependencies ({State.vAccu; separator_hack; loadpath} as st) basena
                   add_dep (Dep_info.Dep.Require file_str)) files
             | None ->
               if not (Loadpath.is_in_coqlib loadpath ?from str) then
-                warning_module_notfound (Library, from, f, str)
+                warning_module_notfound ~loc:(get_loc f loc) (Library, from, str)
           end
         in
         List.iter decl strl;
@@ -286,13 +285,13 @@ let rec find_dependencies ({State.vAccu; separator_hack; loadpath} as st) basena
            in
            List.iter decl l);
         loop ()
-      | External(from,str) ->
+      | External(loc,from,str) ->
         begin match safe_assoc loadpath ~what:External (Some from) f [str] with
         | Some (file :: _) -> add_dep (Dep_info.Dep.Other (canonize ~separator_hack vAccu file))
         | Some [] -> assert false
         | None ->
           if not (Loadpath.is_other_in_coqlib loadpath ~from [str]) then
-            warning_module_notfound (External, Some from, f, [str])
+            warning_module_notfound ~loc:(get_loc f loc) (External, Some from, [str])
         end;
         loop ()
   in
@@ -357,7 +356,7 @@ let sort {State.vAccu; separator_hack; loadpath} =
           match Lexer.coq_action lb with
           | Lexer.Require (from, sl) ->
                 List.iter
-                  (fun s ->
+                  (fun (_,s) ->
                     match safe_assoc loadpath from ~warn_clashes:false file s with
                     | None -> ()
                     | Some l -> List.iter loop l)
diff --git a/tools/coqdep/lib/lexer.mli b/tools/coqdep/lib/lexer.mli
index 21af680674e9..f8038649d770 100644
--- a/tools/coqdep/lib/lexer.mli
+++ b/tools/coqdep/lib/lexer.mli
@@ -12,13 +12,15 @@ type qualid = string list
 
 type load = Logical of string | Physical of string
 
+type loc = { loc_start : int; loc_end : int }
+
 type coq_token =
-  | Require of qualid option * qualid list
+  | Require of qualid option * (loc * qualid) list
   | Declare of string list
   | Load of load
-  | External of qualid * string
+  | External of loc * qualid * string
 
 exception Fin_fichier
-exception Syntax_error of int * int
+exception Syntax_error of loc
 
 val coq_action : Lexing.lexbuf -> coq_token
diff --git a/tools/coqdep/lib/lexer.mll b/tools/coqdep/lib/lexer.mll
index 6e2a09703a9a..a47d78fbfec9 100644
--- a/tools/coqdep/lib/lexer.mll
+++ b/tools/coqdep/lib/lexer.mll
@@ -13,18 +13,20 @@
   open Filename
   open Lexing
 
+  type loc = { loc_start : int; loc_end : int }
+
   type qualid = string list
 
   type load = Logical of string | Physical of string
 
   type coq_token =
-    | Require of qualid option * qualid list
+    | Require of qualid option * (loc * qualid) list
     | Declare of string list
     | Load of load
-    | External of qualid * string
+    | External of loc * qualid * string
 
   exception Fin_fichier
-  exception Syntax_error of int*int
+  exception Syntax_error of loc
 
   let unquote_string s =
     String.sub s 1 (String.length s - 2)
@@ -36,10 +38,18 @@
   let backtrack lexbuf = lexbuf.lex_curr_pos <- lexbuf.lex_start_pos;
     lexbuf.lex_curr_p <- lexbuf.lex_start_p
 
+  let loc_start lexbuf = lexbuf.lex_abs_pos + lexbuf.lex_start_pos
+  let loc_end lexbuf = lexbuf.lex_abs_pos + lexbuf.lex_curr_pos
+
+  let loc lexbuf = { loc_start=loc_start lexbuf; loc_end=loc_end lexbuf}
+
   let syntax_error lexbuf =
     (* abs_pos is position of the start of the buffer in the file
        start/curr_pos are positions in the buffer *)
-    raise (Syntax_error (lexbuf.lex_abs_pos + lexbuf.lex_start_pos, lexbuf.lex_abs_pos + lexbuf.lex_curr_pos))
+    raise (Syntax_error ({
+        loc_start = loc_start lexbuf;
+        loc_end = loc_end lexbuf;
+      }))
 
   let check_valid lexbuf s =
     match Unicode.ident_refutation s with
@@ -144,8 +154,9 @@ and extra_dep_rule from = parse
   | eof
       { syntax_error lexbuf }
   | '"' ([^ '"']+ as f) '"' (*'"'*)
-      { skip_to_dot lexbuf;
-        External (from,f) }
+      { let loc = loc lexbuf in
+        skip_to_dot lexbuf;
+        External (loc,from,f) }
 
 and require_modifiers from = parse
   | "(*"
@@ -220,8 +231,10 @@ and require_file from = parse
   | space+
       { require_file from lexbuf }
   | coq_ident
-      { let name = coq_qual_id_tail [get_ident lexbuf] lexbuf in
-        let qid = coq_qual_id_list [name] lexbuf in
+      { let loc_start = loc_start lexbuf in
+        let name = coq_qual_id_tail [get_ident lexbuf] lexbuf in
+        let loc_end = loc_end lexbuf in
+        let qid = coq_qual_id_list [{loc_start;loc_end},name] lexbuf in
         parse_dot lexbuf;
         Require (from, qid) }
   | eof
@@ -268,8 +281,10 @@ and coq_qual_id_list module_names = parse
   | space+
       { coq_qual_id_list module_names lexbuf }
   | coq_ident
-      { let name = coq_qual_id_tail [get_ident lexbuf] lexbuf in
-        coq_qual_id_list (name :: module_names) lexbuf
+      { let loc_start = loc_start lexbuf in
+        let name = coq_qual_id_tail [get_ident lexbuf] lexbuf in
+        let loc_end = loc_end lexbuf in
+        coq_qual_id_list (({loc_start;loc_end},name) :: module_names) lexbuf
       }
   | eof
       { syntax_error lexbuf }
diff --git a/tools/dune_rule_gen/gen_rules.ml b/tools/dune_rule_gen/gen_rules.ml
index 069caa5b51f4..f9e1b4ad7562 100644
--- a/tools/dune_rule_gen/gen_rules.ml
+++ b/tools/dune_rule_gen/gen_rules.ml
@@ -124,14 +124,9 @@ let main () =
   Format.pp_print_flush fmt ();
   ()
 
-let pr_feedback (fb : Feedback.feedback) =
-  match fb.contents with
-  | Message (_,_,_,msg) -> Format.eprintf "%a" Pp.pp_with msg
-  | _ -> () [@@warning "-4"]
-
 let () =
   Printexc.record_backtrace true;
-  let _ : int = Feedback.add_feeder pr_feedback in
+  let _ : int = Feedback.add_feeder (Feedback.console_feedback_listener Format.err_formatter) in
   try main ()
   with exn ->
     Format.eprintf "[gen_rules] Fatal error:@ @[<2>%a@]@\n%!" Pp.pp_with (CErrors.print exn);

From 241f4b23af8aee918b3e2188c88dfe682fa9e0e1 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Ga=C3=ABtan=20Gilbert?= <gaetan.gilbert@skyskimmer.net>
Date: Wed, 8 Jul 2026 16:03:07 +0200
Subject: [PATCH 20/28] changelog

(cherry picked from commit 7192787afa38d8f7fb3aef034e46bd40c549d728)
---
 .../22231-coqdep-warn-loc-Changed.rst                        | 5 +++++
 1 file changed, 5 insertions(+)
 create mode 100644 doc/changelog/08-vernac-commands-and-options/22231-coqdep-warn-loc-Changed.rst

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
new file mode 100644
index 000000000000..cf743b1d9596
--- /dev/null
+++ b/doc/changelog/08-vernac-commands-and-options/22231-coqdep-warn-loc-Changed.rst
@@ -0,0 +1,5 @@
+- **Changed:**
+  `rocq dep` errors have more readable locations, and warnings have locations
+  (`#22231 <https://github.com/rocq-prover/rocq/pull/22231>`_,
+  fixes `#10815 <https://github.com/rocq-prover/rocq/issues/10815>`_,
+  by Gaëtan Gilbert).

From a65f48385518ee90e9a23263da9f014185ada2ec Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Ga=C3=ABtan=20Gilbert?= <gaetan.gilbert@skyskimmer.net>
Date: Thu, 9 Jul 2026 16:32:56 +0200
Subject: [PATCH 21/28] non-boolean-if warning: mention ctor name in warning
 message

It's not fully ideal as we print `if _ is $ctor` with the ctor name
instead of any notation and without any needed hole arguments but
better than nothing IMO.

(cherry picked from commit 68ff0a7871cbc458f2b107dedaf21aa1ff325f8c)
---
 pretyping/pretyping.ml   | 20 +++++++++++++-------
 test-suite/output/If.out |  4 ++--
 2 files changed, 15 insertions(+), 9 deletions(-)

diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 91b703b6367c..603692598881 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -1405,14 +1405,20 @@ struct
     Cases.compile_cases ?loc ~program_mode:flags.program_mode sty (pretype, sigma) tycon env (po,tml,eqns)
 
   let warn_nonbool_if =
-    let quickfix ~loc (cloc, pp) =
-      let qf loc = let loc = Loc.after loc 0 0 in [Quickfix.make ~loc pp] in
-      Option.cata qf [] cloc in
+    let quickfix ~loc:_ (cloc, ctor) =
+      match cloc with
+      | None -> []
+      | Some cloc ->
+        let loc = Loc.after cloc 0 0 in
+        let pp = Pp.(str " is " ++ Nametab.pr_global_env Id.Set.empty (ConstructRef ctor)) in
+        [Quickfix.make ~loc pp]
+    in
     CWarnings.create ~name:"non-boolean-if" ~category:Deprecation.Version.v9_3
       ~quickfix
-      (fun _ ->
-         strbrk "The \"if <c> then _\" syntax for non boolean guard is deprecated. "
-         ++ strbrk "Use \"if <c> is <first_constructor> then _\" instead.")
+      (fun (_,ctor) ->
+         str "The \"if <c> then _\" syntax for non boolean guard is deprecated." ++ spc() ++
+         fmt "Use \"if <c> is %t then _\" instead."
+           (fun () -> Nametab.pr_global_env Id.Set.empty (ConstructRef ctor)))
 
   let pretype_if self (c, (na, po), b1, b2) =
     fun ?loc ~flags tycon env sigma ->
@@ -1436,7 +1442,7 @@ struct
           | Some bool -> GlobRef.CanOrd.equal (IndRef ind) bool in
       if not indf_is_bool then
         let cloc = loc_of_glob_constr c in
-        warn_nonbool_if ?loc (cloc, Pp.str " is " ++ Id.print cstrs.(0).cs_name) in
+        warn_nonbool_if ?loc (cloc, fst cstrs.(0).cs_cstr) in
     let arsgn, indr =
       let arsgn = get_arity !!env indf in
       (* Make dependencies from arity signature impossible *)
diff --git a/test-suite/output/If.out b/test-suite/output/If.out
index 5b5605ebd0d5..b2fed907d8f8 100644
--- a/test-suite/output/If.out
+++ b/test-suite/output/If.out
@@ -1,8 +1,8 @@
 if true then 1 else 0
      : nat
 File "./output/If.v", line 3, characters 6-24:
-Warning: The "if <c> then _" syntax for non boolean guard is deprecated. Use
-"if <c> is <first_constructor> then _" instead.
+Warning: The "if <c> then _" syntax for non boolean guard is deprecated.
+Use "if <c> is O then _" instead.
 [non-boolean-if,deprecated-since-9.3,deprecated,default]
 Quickfix:
 Replace File "./output/If.v", line 3, characters 10-10 with  is O

From 2fdd040cd24e0f6559776dec0e443f939449f113 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Ga=C3=ABtan=20Gilbert?= <gaetan.gilbert@skyskimmer.net>
Date: Fri, 10 Jul 2026 12:36:30 +0200
Subject: [PATCH 22/28] Fix dune runtest for dune 3.24

cf https://github.com/ocaml/dune/issues/15458#issuecomment-4934344267
(the `%{pkg` suggestion can't be used until we depend on 3.24)

(cherry picked from commit 84bf942a2065e2f13c90ebcc279310722863414d)
---
 test-suite/dune | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/test-suite/dune b/test-suite/dune
index eacf93cb714c..44c8049dac43 100644
--- a/test-suite/dune
+++ b/test-suite/dune
@@ -10,7 +10,8 @@
 (rule
  (targets test_suite_config.inc)
  (mode (promote (until-clean)))
- (action (with-stdout-to %{targets} (run tools/coq_config_to_make.exe %{bin:rocq}))))
+ (deps (package rocq-runtime))
+ (action (with-stdout-to %{targets} (run tools/coq_config_to_make.exe rocq))))
 
 (rule
  (targets summary.log)

From 9ee3f4d5c07b7846283bf5da1ef88cb75a1d3468 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Ga=C3=ABtan=20Gilbert?= <gaetan.gilbert@skyskimmer.net>
Date: Fri, 10 Jul 2026 12:45:24 +0200
Subject: [PATCH 23/28] missing-proof-command warning mentions Default Proof
 Using if relevant

(cherry picked from commit 9412aba2aba80d419eb26453d660d76826f0e254)
---
 test-suite/output/bug_11608.out |  1 +
 vernac/vernactypes.ml           | 14 +++++++++++---
 2 files changed, 12 insertions(+), 3 deletions(-)

diff --git a/test-suite/output/bug_11608.out b/test-suite/output/bug_11608.out
index 074a66154abe..3ee30d6d1e8d 100644
--- a/test-suite/output/bug_11608.out
+++ b/test-suite/output/bug_11608.out
@@ -1,5 +1,6 @@
 File "./output/bug_11608.v", line 10, characters 4-40:
 Warning: This interactive proof is not started by the "Proof" command.
+Default Proof Using "(Type)" will be ignored.
 [missing-proof-command,fragile,default]
 Quickfix:
 Replace File "./output/bug_11608.v", line 10, characters 4-4 with Proof.
diff --git a/vernac/vernactypes.ml b/vernac/vernactypes.ml
index de650bdabcf1..de4d2a8ea039 100644
--- a/vernac/vernactypes.ml
+++ b/vernac/vernactypes.ml
@@ -63,19 +63,27 @@ module Proof = struct
     | None -> CErrors.user_err (Pp.str "Command not supported (No proof-editing in progress).")
     | Some stack -> LStack.pop stack
 
-  let quickfix_missing_proof ~loc () =
+  let quickfix_missing_proof ~loc _ =
     (* quickfix is purely additive so the loc is 0 characters long, at the beginning of the command. *)
     let loc = { loc with Loc.ep = loc.Loc.bp } in
     [Quickfix.make ~loc Pp.(str "Proof." ++ fnl())]
 
   let warn_missing_proof = CWarnings.create ~name:"missing-proof-command" ~category:CWarnings.CoreCategories.fragile
       ~quickfix:quickfix_missing_proof
-      Pp.(fun () -> str "This interactive proof is not started by the \"Proof\" command.")
+      Pp.(fun default_using ->
+          str "This interactive proof is not started by the \"Proof\" command." ++
+          (match default_using with
+           | None -> mt()
+           | Some using ->
+             spc() ++ str "Default Proof Using " ++ quote (Ppvernac.pr_using using) ++ str " will be ignored."))
 
   let check_late_init ?loc p =
     if Option.has_some @@ Declare.Proof.has_late_init p then p
     else begin
-      warn_missing_proof ?loc ();
+      let missing_using =
+        if Global.sections_are_opened() then Proof_using.get_default_proof_using() else None
+      in
+      warn_missing_proof ?loc missing_using;
       Declare.Proof.finish_late_init p Implicit
     end
 

From e28320a2d733060d1743b7b9fe70612a561001af Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Ga=C3=ABtan=20Gilbert?= <gaetan.gilbert@skyskimmer.net>
Date: Thu, 9 Jul 2026 16:40:09 +0200
Subject: [PATCH 24/28] Undeprecate `...` ("Proof with")

It seems this was more used than expected.

(cherry picked from commit 9dd02ea6bff1bb1c0c39cd2e7ff9c6271e61d430)
---
 .../22251-underp-proof-with-Changed.rst       |  4 ++++
 vernac/comTactic.ml                           | 22 +++----------------
 2 files changed, 7 insertions(+), 19 deletions(-)
 create mode 100644 doc/changelog/04-tactics/22251-underp-proof-with-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
new file mode 100644
index 000000000000..ac80a1ad7fea
--- /dev/null
+++ b/doc/changelog/04-tactics/22251-underp-proof-with-Changed.rst
@@ -0,0 +1,4 @@
+- **Changed:**
+  `...` (:cmd:`Proof with`) is not deprecated anymore and is expected to remain available
+  (`#22251 <https://github.com/rocq-prover/rocq/pull/22251>`_,
+  by Gaëtan Gilbert).
diff --git a/vernac/comTactic.ml b/vernac/comTactic.ml
index 79859d5b1281..81e746109c3f 100644
--- a/vernac/comTactic.ml
+++ b/vernac/comTactic.ml
@@ -41,31 +41,15 @@ let { Goptions.get = print_info_trace } =
     ~value:None
     ()
 
-let warn_end_tac =
-  CWarnings.create_warning ~name:"deprecated-end-tac" ~from:[Deprecation.Version.v9_2] ()
-
-let pp_warn_end_tac =
-  let pptac end_tac =
-    let env = Global.env() in
-    let sigma = Evd.from_env env in
-    let pptac = Gentactic.print_glob env sigma end_tac in
-    Pp.(str ";" ++ spc() ++ pptac ++ str ".")
-  in
-  CWarnings.create_in warn_end_tac
-    ~quickfix:(fun ~loc end_tac -> [Quickfix.make ~loc (pptac end_tac)])
-    Pp.(fun end_tac ->
-      fmt "Using \"...\" is deprecated, use \"%t\" instead" (fun () -> pptac end_tac))
-
-let warn_end_tac ?loc end_tac =
+let check_end_tac ?loc end_tac =
   match end_tac with
   | None -> CErrors.user_err ?loc Pp.(str "This \"...\" is useless, use \".\" instead.")
-  | Some end_tac ->
-    pp_warn_end_tac ?loc end_tac
+  | Some _ -> ()
 
 let use_end_tac ~with_end_tac end_tac =
   if not with_end_tac.CAst.v then None
   else begin
-    warn_end_tac ?loc:with_end_tac.loc end_tac;
+    check_end_tac ?loc:with_end_tac.loc end_tac;
     Option.map Gentactic.interp end_tac
   end
 

From 0d18992891a0722277a22079776ed578b357636b Mon Sep 17 00:00:00 2001
From: Jason Gross <jason@theorem.dev>
Date: Wed, 24 Jun 2026 21:58:38 +0000
Subject: [PATCH 25/28] feat: add Set Printing All Assumptions flag

When enabled, Print Assumptions reports theory assumptions
(impredicative set, rewrite rules, type-in-type) based on
per-definition typing flags rather than the current environment
settings. This also makes IndicesNotMattering show regardless of
the current Indices Matter setting.

Previously, theory assumptions were only shown based on the global
environment state, which meant e.g. a definition typed with
-impredicative-set would not show "Set is impredicative" if imported
into a predicative environment.

Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_019ttctspSoVoquHLQtbPVZw
(cherry picked from commit 396c77536a3b402dd8c927d6514facc3100baf4c)
---
 ...-JasonGross-print-assumptions-all-flags.sh |  1 +
 printing/printer.ml                           | 37 ++++++++++++++++---
 printing/printer.mli                          | 11 +++++-
 test-suite/output/PrintAllAssumptions.out     |  3 ++
 test-suite/output/PrintAllAssumptions.v       | 10 +++++
 test-suite/output/indices_matter.out          |  3 ++
 test-suite/output/indices_matter.v            |  8 ++++
 test-suite/prerequisite/impred_set_prereq.v   |  2 +
 vernac/assumptions.ml                         | 25 +++++++++++--
 vernac/assumptions.mli                        |  3 +-
 vernac/vernacentries.ml                       |  4 +-
 11 files changed, 94 insertions(+), 13 deletions(-)
 create mode 100644 dev/ci/user-overlays/22164-JasonGross-print-assumptions-all-flags.sh
 create mode 100644 test-suite/output/PrintAllAssumptions.out
 create mode 100644 test-suite/output/PrintAllAssumptions.v
 create mode 100644 test-suite/prerequisite/impred_set_prereq.v

diff --git a/dev/ci/user-overlays/22164-JasonGross-print-assumptions-all-flags.sh b/dev/ci/user-overlays/22164-JasonGross-print-assumptions-all-flags.sh
new file mode 100644
index 000000000000..1931c3015303
--- /dev/null
+++ b/dev/ci/user-overlays/22164-JasonGross-print-assumptions-all-flags.sh
@@ -0,0 +1 @@
+overlay metarocq https://github.com/JasonGross/metacoq print-assumptions-all-flags 22164
diff --git a/printing/printer.ml b/printing/printer.ml
index 94bdb06ce4c4..8379352eca6a 100644
--- a/printing/printer.ml
+++ b/printing/printer.ml
@@ -610,6 +610,12 @@ let pr_ne_evar_set ?(flags=current_combined()) hd tl sigma l =
 (* Printer function for sets of Assumptions.assumptions.
    It is used primarily by the Print Assumptions command. *)
 
+let { Goptions.get = print_all_assumptions } =
+  Goptions.declare_bool_option_and_ref
+    ~key:["Printing";"All";"Assumptions"]
+    ~value:false
+    ()
+
 type axiom =
   | Constant of Constant.t
   | Positive of MutInd.t
@@ -668,10 +674,29 @@ end
 module ContextObjectSet = Set.Make (OrderedContextObject)
 module ContextObjectMap = Map.Make (OrderedContextObject)
 
-let pr_assumptionset ?(flags=current_combined()) env sigma s =
+type theory_assumptions = {
+  has_impredicative_set : bool;
+  has_rewrite_rules : bool;
+  has_type_in_type : bool;
+}
+
+let pr_assumptionset ?(flags=current_combined()) env sigma theory_info s =
+  let print_all = print_all_assumptions () in
+  let dominated_by_env ax =
+    match ax with
+    | IndicesNotMattering _ -> not print_all && not (indices_matter env)
+    | _ -> false
+  in
+  let s = ContextObjectMap.filter (fun k _v -> match k with
+    | Axiom (ax, _) -> not (dominated_by_env ax)
+    | _ -> true) s
+  in
+  let show_theory_impredicative_set = (print_all && theory_info.has_impredicative_set) || is_impredicative_set env in
+  let show_theory_rewrite_rules = (print_all && theory_info.has_rewrite_rules) || rewrite_rules_allowed env in
+  let show_theory_type_in_type = (print_all && theory_info.has_type_in_type) || type_in_type env in
   if ContextObjectMap.is_empty s &&
-       not (rewrite_rules_allowed env) &&
-       not (is_impredicative_set env) then
+       not show_theory_rewrite_rules &&
+       not show_theory_impredicative_set then
     str "Closed under the global context"
   else
     let safe_pr_constant env kn =
@@ -751,17 +776,17 @@ let pr_assumptionset ?(flags=current_combined()) env sigma s =
       ContextObjectMap.fold fold s ([], [], [], [])
     in
     let theory =
-      if is_impredicative_set env then
+      if show_theory_impredicative_set then
         [str "Set is impredicative"]
       else []
     in
     let theory =
-      if rewrite_rules_allowed env then
+      if show_theory_rewrite_rules then
         str "Rewrite rules are allowed (subject reduction might be broken)" :: theory
       else theory
     in
     let theory =
-      if type_in_type env then
+      if show_theory_type_in_type then
         str "Type hierarchy is collapsed (logic is inconsistent)" :: theory
       else theory
     in
diff --git a/printing/printer.mli b/printing/printer.mli
index 5d5dca50608f..b855f8a1e3dc 100644
--- a/printing/printer.mli
+++ b/printing/printer.mli
@@ -226,6 +226,9 @@ val pr_ne_evar_set : ?flags:PrintingFlags.t ->
   Evar.Set.t -> Pp.t
 
 (** Declarations for the "Print Assumption" command *)
+
+val print_all_assumptions : unit -> bool
+
 type axiom =
   | Constant of Constant.t (* An axiom or a constant. *)
   | Positive of MutInd.t (* A mutually inductive definition which has been assumed positive. *)
@@ -244,8 +247,14 @@ module ContextObjectSet : CSet.ExtS with type elt = context_object
 module ContextObjectMap : CMap.ExtS
   with type key = context_object and module Set := ContextObjectSet
 
+type theory_assumptions = {
+  has_impredicative_set : bool;
+  has_rewrite_rules : bool;
+  has_type_in_type : bool;
+}
+
 val pr_assumptionset : ?flags:PrintingFlags.t ->
-  env -> evar_map -> types ContextObjectMap.t -> Pp.t
+  env -> evar_map -> theory_assumptions -> types ContextObjectMap.t -> Pp.t
 
 val pr_typing_flags : Declarations.typing_flags -> Pp.t
 
diff --git a/test-suite/output/PrintAllAssumptions.out b/test-suite/output/PrintAllAssumptions.out
new file mode 100644
index 000000000000..98cabd21001c
--- /dev/null
+++ b/test-suite/output/PrintAllAssumptions.out
@@ -0,0 +1,3 @@
+Closed under the global context
+Theory:
+Set is impredicative
diff --git a/test-suite/output/PrintAllAssumptions.v b/test-suite/output/PrintAllAssumptions.v
new file mode 100644
index 000000000000..ee25263bc865
--- /dev/null
+++ b/test-suite/output/PrintAllAssumptions.v
@@ -0,0 +1,10 @@
+(** Test for Set Printing All Assumptions *)
+Require Import TestSuite.impred_set_prereq.
+
+(** Without the flag, impredicative_set is not in the current env,
+    so Print Assumptions hides the theory dependency *)
+Print Assumptions impred_def.
+
+(** With the flag, per-definition theory info is shown *)
+Set Printing All Assumptions.
+Print Assumptions impred_def.
diff --git a/test-suite/output/indices_matter.out b/test-suite/output/indices_matter.out
index eff79ca98662..e1e9f69d49d5 100644
--- a/test-suite/output/indices_matter.out
+++ b/test-suite/output/indices_matter.out
@@ -3,3 +3,6 @@ M.X relies on indices not mattering.
 Axioms:
 M.X relies on indices not mattering.
 Closed under the global context
+Closed under the global context
+Axioms:
+M.X relies on indices not mattering.
diff --git a/test-suite/output/indices_matter.v b/test-suite/output/indices_matter.v
index 1a6393627f59..e08cac477aa4 100644
--- a/test-suite/output/indices_matter.v
+++ b/test-suite/output/indices_matter.v
@@ -10,3 +10,11 @@ Module SetIndicesMatter.
   Unset Indices Matter.
   Print Assumptions M.X.
 End SetIndicesMatter.
+
+(* Test Set Printing All Assumptions *)
+Module PrintingAllAssumptions.
+  Unset Indices Matter.
+  Print Assumptions M.X.
+  Set Printing All Assumptions.
+  Print Assumptions M.X.
+End PrintingAllAssumptions.
diff --git a/test-suite/prerequisite/impred_set_prereq.v b/test-suite/prerequisite/impred_set_prereq.v
new file mode 100644
index 000000000000..96a0638c7923
--- /dev/null
+++ b/test-suite/prerequisite/impred_set_prereq.v
@@ -0,0 +1,2 @@
+(* -*- coq-prog-args: ("-impredicative-set"); -*- *)
+Definition impred_def : Set := forall X : Set, X -> X.
diff --git a/vernac/assumptions.ml b/vernac/assumptions.ml
index 313a5014e715..2e2058b9bbec 100644
--- a/vernac/assumptions.ml
+++ b/vernac/assumptions.ml
@@ -374,6 +374,13 @@ let assumptions ?(add_opaque=false) ?(add_transparent=false) access st grs =
   (* Only keep the transitive dependencies *)
   let (_, graph, ax2ty) = traverse access grs in
   let open GlobRef in
+  let has_impredicative_set = ref false in
+  let has_rewrite_rules = ref false in
+  let has_type_in_type = ref false in
+  let collect_theory_flags (tf : Declarations.typing_flags) =
+    if tf.impredicative_set then has_impredicative_set := true;
+    if not tf.check_universes then has_type_in_type := true
+  in
   let fold obj contents accu = match obj with
   | VarRef id ->
     let decl = Global.lookup_named id in
@@ -383,6 +390,11 @@ let assumptions ?(add_opaque=false) ?(add_transparent=false) access st grs =
     else accu
   | ConstRef kn ->
       let cb = lookup_constant kn in
+      collect_theory_flags cb.const_typing_flags;
+      begin match cb.const_body with
+        | Symbol _ -> has_rewrite_rules := true
+        | _ -> ()
+      end;
       let accu =
         if cb.const_typing_flags.check_guarded then accu
         else
@@ -409,6 +421,7 @@ let assumptions ?(add_opaque=false) ?(add_transparent=false) access st grs =
       accu
   | IndRef (m,_) | ConstructRef ((m,_),_) ->
       let mind = lookup_mind m in
+      collect_theory_flags mind.mind_typing_flags;
       let accu =
         if mind.mind_typing_flags.check_positive then accu
         else
@@ -434,11 +447,17 @@ let assumptions ?(add_opaque=false) ?(add_transparent=false) access st grs =
           ContextObjectMap.add (Axiom (UIP m, l)) Constr.mkProp accu
       in
       let accu =
-        if not (Environ.indices_matter (Global.env ())) then accu
-        else if not (Array.exists (fun mip -> mip.mind_relies_on_indices_not_mattering) mind.mind_packets) then accu
+        if not (Array.exists (fun mip -> mip.mind_relies_on_indices_not_mattering) mind.mind_packets) then accu
         else
           let l = try GlobRef.Map_env.find obj ax2ty with Not_found -> [] in
           ContextObjectMap.add (Axiom (IndicesNotMattering m, l)) Constr.mkProp accu
       in
       accu
-  in GlobRef.Map_env.fold fold graph ContextObjectMap.empty
+  in
+  let map = GlobRef.Map_env.fold fold graph ContextObjectMap.empty in
+  let theory = {
+    has_impredicative_set = !has_impredicative_set;
+    has_rewrite_rules = !has_rewrite_rules;
+    has_type_in_type = !has_type_in_type;
+  } in
+  (theory, map)
diff --git a/vernac/assumptions.mli b/vernac/assumptions.mli
index 9e80a9942ccb..5fa3ad65c6a7 100644
--- a/vernac/assumptions.mli
+++ b/vernac/assumptions.mli
@@ -31,4 +31,5 @@ val traverse :
    {!traverse} also applies. *)
 val assumptions :
   ?add_opaque:bool -> ?add_transparent:bool -> Global.indirect_accessor ->
-  TransparentState.t -> GlobRef.t list -> types ContextObjectMap.t
+  TransparentState.t -> GlobRef.t list ->
+  theory_assumptions * types ContextObjectMap.t
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index f2a305d9d288..0d8ea9672857 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -2364,9 +2364,9 @@ let vernac_print =
     (* Prints all the axioms and section variables used by a term *)
     let st = Conv_oracle.get_transp_state (Environ.oracle env) in
     let grs = List.map smart_global rs in
-    let nassums =
+    let (theory, nassums) =
       Assumptions.assumptions opaque_access st ~add_opaque:o ~add_transparent:t grs in
-    Printer.pr_assumptionset env sigma nassums
+    Printer.pr_assumptionset env sigma theory nassums
   | PrintStrategy r -> no_state @@ fun () -> print_strategy r
   | PrintRegistered -> no_state print_registered
   | PrintRegisteredSchemes -> no_state print_registered_schemes

From a21531efb688dcec2b0ce4db98ce40fe0e32e2b7 Mon Sep 17 00:00:00 2001
From: Jason Gross <jason@theorem.dev>
Date: Wed, 8 Jul 2026 14:00:40 +0000
Subject: [PATCH 26/28] Add documentation and changelog

Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_019ttctspSoVoquHLQtbPVZw
(cherry picked from commit fc9bc41984d426613695b5a3478057c74045932c)
---
 .../22164-print-assumptions-all-flags-Added.rst   |  7 +++++++
 doc/sphinx/proof-engine/vernacular-commands.rst   | 15 +++++++++++++++
 2 files changed, 22 insertions(+)
 create mode 100644 doc/changelog/08-vernac-commands-and-options/22164-print-assumptions-all-flags-Added.rst

diff --git a/doc/changelog/08-vernac-commands-and-options/22164-print-assumptions-all-flags-Added.rst b/doc/changelog/08-vernac-commands-and-options/22164-print-assumptions-all-flags-Added.rst
new file mode 100644
index 000000000000..bb44bfee1da3
--- /dev/null
+++ b/doc/changelog/08-vernac-commands-and-options/22164-print-assumptions-all-flags-Added.rst
@@ -0,0 +1,7 @@
+- **Added:**
+  ``Printing All Assumptions`` flag making :cmd:`Print Assumptions` report
+  theory assumptions (impredicativity of :g:`Set`, rewrite rules, disabled
+  universe checking, indices not mattering) according to each definition's
+  typing flags in addition to the settings of the current environment
+  (`#22164 <https://github.com/rocq-prover/rocq/pull/22164>`_,
+  by Jason Gross).
diff --git a/doc/sphinx/proof-engine/vernacular-commands.rst b/doc/sphinx/proof-engine/vernacular-commands.rst
index d5b550ed6786..5d990b2bd188 100644
--- a/doc/sphinx/proof-engine/vernacular-commands.rst
+++ b/doc/sphinx/proof-engine/vernacular-commands.rst
@@ -454,6 +454,21 @@ Requests to the environment
    The message "Closed under the global context" indicates that all the theorems and
    definitions have no dependencies.
 
+.. flag:: Printing All Assumptions
+
+   Turn this :term:`flag` on to make :cmd:`Print Assumptions` report
+   theory assumptions (impredicativity of :g:`Set`, rewrite rules,
+   disabled universe checking, indices not mattering) according to the
+   typing flags each dependency was typechecked with, in addition to
+   the settings of the current environment.  For instance, a definition
+   typechecked with ``-impredicative-set`` is reported as assuming the
+   impredicativity of :g:`Set` even when it is imported into a
+   predicative environment, and an inductive type relying on indices
+   not mattering is reported even when :flag:`Indices Matter` is off in
+   the current environment (without this flag, such inductive types are
+   reported only when :flag:`Indices Matter` is currently on, since an
+   environment where indices do not matter subsumes that assumption).
+
 .. cmd:: Print Opaque Dependencies {+ @reference }
 
    Displays the assumptions and opaque constants that :n:`@reference` depends on.

From d2df2f518ae009f43c6cf7b158f6ee8b8f8f4b90 Mon Sep 17 00:00:00 2001
From: Enrico Tassi <Enrico.Tassi@Inria.fr>
Date: Wed, 15 Jul 2026 13:00:21 +0200
Subject: [PATCH 27/28] CACHEKEY

---
 .gitlab-ci.yml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index 784c6a9ed9d1..059fa1400653 100644
--- a/.gitlab-ci.yml
+++ b/.gitlab-ci.yml
@@ -40,8 +40,8 @@ variables:
   # The $hash is the first 10 characters of the md5 of the Dockerfile. e.g.
   # echo $(md5sum dev/ci/docker/old_ubuntu_lts/Dockerfile | head -c 10)
   # echo $(md5sum dev/ci/docker/edge_ubuntu/Dockerfile | head -c 10)
-  BASE_CACHEKEY: "old_ubuntu_lts-V2026-07-06-00242ff07f"
-  EDGE_CACHEKEY: "edge_ubuntu-V2026-07-06-62b9804f8c"
+  BASE_CACHEKEY: "old_ubuntu_lts-v9.3-V2026-07-06-00242ff07f"
+  EDGE_CACHEKEY: "edge_ubuntu-v9.3-V2026-07-06-62b9804f8c"
   BASE_IMAGE: "$CI_REGISTRY_IMAGE:$BASE_CACHEKEY"
   EDGE_IMAGE: "$CI_REGISTRY_IMAGE:$EDGE_CACHEKEY"
 

From 45d6e787c952b52b2f965b1444bbe504e6d0f178 Mon Sep 17 00:00:00 2001
From: Enrico Tassi <Enrico.Tassi@Inria.fr>
Date: Wed, 15 Jul 2026 15:33:39 +0200
Subject: [PATCH 28/28] bump ci pin for metarocq

---
 dev/ci/ci-basic-overlay.sh | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/dev/ci/ci-basic-overlay.sh b/dev/ci/ci-basic-overlay.sh
index 9a49ca14d100..f955c4f651b4 100644
--- a/dev/ci/ci-basic-overlay.sh
+++ b/dev/ci/ci-basic-overlay.sh
@@ -368,7 +368,7 @@ project atbr 'https://github.com/coq-community/atbr' '1806f95dd68b953312cbee4422
 ########################################################################
 # metarocq
 ########################################################################
-project metarocq 'https://github.com/MetaRocq/metarocq' '2d501a9787ff3560f9872340bf0c3628edc58ed4'
+project metarocq 'https://github.com/MetaRocq/metarocq' '9242c14bc377611a56d45283977ea754fd499c47'
 # Contact @mattam82, @yforster on github
 
 ########################################################################