From f0cc9038fd3586a9a63173d68452ce8fcdb3a5b4 Mon Sep 17 00:00:00 2001
From: Pierre Roux <pierre.roux@onera.fr>
Date: Tue, 31 Mar 2026 16:43:45 +0200
Subject: [PATCH] Adapt to https://github.com/rocq-prover/rocq/pull/21851

---
 tests/output/NumbersSyntax.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/tests/output/NumbersSyntax.v b/tests/output/NumbersSyntax.v
index ea6dcb6..ba37f0d 100644
--- a/tests/output/NumbersSyntax.v
+++ b/tests/output/NumbersSyntax.v
@@ -1,4 +1,4 @@
-Require Import ZArith.
+From Stdlib Require Import ZArith.
 Require Import Bignums.BigQ.BigQ.
 
 Open Scope bigN_scope.