Merge pull request #110 from rocq-community/rocq21851

proux01 · web-flow · commit 36cd7009759b · 2026-03-31T17:07:58.000+02:00
Adapt to rocq-prover/rocq#21851
diff --git 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.

Original file line number	Diff line number	Diff line change
`@@ -1,4 +1,4 @@`
`1`		`-Require Import ZArith.`
	`1`	`+From Stdlib Require Import ZArith.`
`2`	`2`	`Require Import Bignums.BigQ.BigQ.`
`3`	`3`
`4`	`4`	`Open Scope bigN_scope.`