rocq-prover · gares · Jul 8, 2026 · Jul 8, 2026 · Jul 9, 2026 · Jul 9, 2026
@@ -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

@@ -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-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"
 

@@ -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) $(WITHJOBS) dune exec -- sphinx-build -q -W -b indices doc/sphinx doc/refman-indices
+
 corelib-html: dunestrap
 	dune build @corelib-html
 

@@ -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
 
 ########################################################################

@@ -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.

@@ -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
 

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
@@ -0,0 +1 @@
+overlay metarocq https://github.com/JasonGross/metacoq print-assumptions-all-flags 22164
@@ -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
@@ -71,6 +73,71 @@ 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,
+    // a simpler, markdown documentation
+    "documentation": string,
+  }
+}
+```
+
+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", Literal]
+  | ["Reference", Reference]
+  | ["Alternative", Alternative]
+  | ["Repeat", Repeat]
+
+// the literal string
+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 = {
+  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 = {
+  children: Syntax[]
+}
+
+// repetition of a list of syntax nodes
+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/changelog/04-tactics/22251-underp-proof-with-Changed.rst 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/...elog/08-vernac-commands-and-options/22164-print-assumptions-all-flags-Added.rst b/...elog/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/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
@@ -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).
diff --git a/doc/changelog/11-corelib/22221-template-scheme-univs-Fixed.rst 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).
@@ -60,6 +60,7 @@
     'sphinx.ext.mathjax',
     'sphinx.ext.todo',
     'sphinxcontrib.bibtex',
+    'sphinx_markdown_builder',
     'rocqrst.rocqdomain'
 ]
 
@@ -211,9 +212,10 @@ def setup(app):
     'versions': [
         ("dev", "https://rocq-prover.org/doc/master/refman/"),
         ("stable", "https://rocq-prover.org/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.3", "https://rocq-prover.org/doc/v9.3/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/"),

@@ -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.

@@ -46,7 +46,7 @@ RBRACE: '}';
 ESCAPED: '%{' | '%}' | '%|' | '`%{' | '@%{' |
   '%|-' | '%|->' | '%||' | '%|||' | '%||||';  // for SSR
 PIPE: '|';
-ATOM: '@' | '_' | ~[@_{}| ]+;
+ATOM: '@' | '_' | ~[@_{}| ]+ ('_' ~[@_{}| ]+)*;
 ID: '@' ('_'? [a-zA-Z0-9])+;
 SUB: '_' '_' [a-zA-Z0-9]+;
 WHITESPACE: ' '+;
@@ -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()
Original file line number	Diff line number	Diff line change
		@@ -0,0 +1 @@
		overlay metarocq https://github.com/JasonGross/metacoq print-assumptions-all-flags 22164