From b4b1daac69670870d026fe69cb1f625ced7bb5b0 Mon Sep 17 00:00:00 2001 From: Pierre Roux Date: Mon, 13 Jul 2026 15:21:23 +0200 Subject: [PATCH] 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..b4ee50549 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 OldCoqPrefix. (* TODO: handle when requiring Rocq >= 9.4 *) + (* Coqlib *) Extract Inlined Constant Coqlib.proj_sumbool => "(fun x -> x)".