From 946958870512a576a7c0df7dd0dd5e0bf2f85d9c Mon Sep 17 00:00:00 2001
From: Pierre Roux <pierre.roux@onera.fr>
Date: Mon, 13 Jul 2026 15:21:23 +0200
Subject: [PATCH 1/2] Adapt to rocq-prover/rocq#22271

Adapt to https://github.com/rocq-prover/rocq/pull/22271
---
 extraction/extraction.v | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/extraction/extraction.v b/extraction/extraction.v
index c01426e6a..d0b0c30b3 100644
--- a/extraction/extraction.v
+++ b/extraction/extraction.v
@@ -27,6 +27,8 @@ Require Initializers.
 (* Standard lib *)
 From Coq Require Import ExtrOcamlBasic ExtrOcamlNativeString.
 
+Set Extraction Prefix "Coq".  (* TODO: handle and remove when requiring Rocq >= 9.4 *)
+
 (* Coqlib *)
 Extract Inlined Constant Coqlib.proj_sumbool => "(fun x -> x)".
 

From 0182963b251f9c5fde991da107d246eac86ec7a9 Mon Sep 17 00:00:00 2001
From: Xavier Leroy <xavier.leroy@college-de-france.fr>
Date: Mon, 10 Aug 2026 10:54:54 +0200
Subject: [PATCH 2/2] Adapt to rocq-prover/rocq#22271 continued

---
 Makefile                | 6 +++++-
 extraction/extraction.v | 2 +-
 2 files changed, 6 insertions(+), 2 deletions(-)

diff --git a/Makefile b/Makefile
index 82af3678a..4d7be5f42 100644
--- a/Makefile
+++ b/Makefile
@@ -86,10 +86,14 @@ MenhirLib/%.vo: COQCOPTS+=-w -deprecated-syntactic-definition -w -deprecated-sin
 #    warning introduced in 8.20, no alternative before 8.20
 # deprecated-from-Coq:
 #    see above
+# unknown-option:
+#    the "Set Extraction Prefix" command was introduced in 9.4
+
 COQEXTRACTOPTS ?= \
   -w -change-dir-deprecated \
   -w -extraction-default-directory \
-  -w -deprecated-from-Coq
+  -w -deprecated-from-Coq  \
+  -w -unknown-option
 
 ifneq ($(INSTALL_COQDEV),true)
 # Disable costly generation of .cmx files, which are not used locally
diff --git a/extraction/extraction.v b/extraction/extraction.v
index d0b0c30b3..a7c529670 100644
--- a/extraction/extraction.v
+++ b/extraction/extraction.v
@@ -27,7 +27,7 @@ Require Initializers.
 (* Standard lib *)
 From Coq Require Import ExtrOcamlBasic ExtrOcamlNativeString.
 
-Set Extraction Prefix "Coq".  (* TODO: handle and remove when requiring Rocq >= 9.4 *)
+Set Extraction Prefix "Coq".  (* prefix changed to "Rocq" in 9.4 *)
 
 (* Coqlib *)
 Extract Inlined Constant Coqlib.proj_sumbool => "(fun x -> x)".