From 3c7c0bb08d406d4addfc0ac68dce45bf7c5cb7e9 Mon Sep 17 00:00:00 2001
From: Pierre Letouzey
Date: Wed, 11 Apr 2018 09:58:56 +0200
Subject: WIP: adapt Numeral Notation to synchronized prim notations

---
 test-suite/interactive/PrimNotation.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'test-suite/interactive')

diff --git a/test-suite/interactive/PrimNotation.v b/test-suite/interactive/PrimNotation.v
index ca8cba67d5..4c81095c68 100644
--- a/test-suite/interactive/PrimNotation.v
+++ b/test-suite/interactive/PrimNotation.v
@@ -7,7 +7,7 @@ Delimit Scope Z_scope with Z.
 Open Scope Z_scope.
 Check 0.
 (* 0 : nat *)
-Require BinNums.
+Require BinInt.
 Check 0.
 (* 0 : BinNums.Z *)
 Back 2.
-- 
cgit v1.2.3