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.