1 files changed, 0 insertions, 21 deletions
diff --git a/test-suite/success/NumberScopes.v b/test-suite/success/NumberScopes.v
index 6d787210..15586374 100644
--- a/test-suite/success/NumberScopes.v
+++ b/test-suite/success/NumberScopes.v
@@ -39,24 +39,3 @@ Definition f_nat (x:nat) := x.
 Definition f_nat' (x:Nat.t) := x.
 Check (f_nat 1).
 Check (f_nat' 1).
-
-Require Import BigN.
-Check (BigN.add 1 2).
-Check (BigN.add_comm 1 2).
-Check (BigN.min_comm 1 2).
-Definition f_bigN (x:bigN) := x.
-Check (f_bigN 1).
-
-Require Import BigZ.
-Check (BigZ.add 1 2).
-Check (BigZ.add_comm 1 2).
-Check (BigZ.min_comm 1 2).
-Definition f_bigZ (x:bigZ) := x.
-Check (f_bigZ 1).
-
-Require Import BigQ.
-Check (BigQ.add 1 2).
-Check (BigQ.add_comm 1 2).
-Check (BigQ.min_comm 1 2).
-Definition f_bigQ (x:bigQ) := x.
-Check (f_bigQ 1).
-\ No newline at end of file