1 files changed, 2 insertions, 2 deletions
diff --git a/contrib/dp/tests.v b/contrib/dp/tests.v
index d12203803..10b6f0d83 100644
--- a/contrib/dp/tests.v
+++ b/contrib/dp/tests.v
@@ -3,7 +3,6 @@ Reset Initial.
 Require Import ZArith.
 Require Import Classical.
 
-
 (* First example with the 0 and the equality translated *)
 
 Goal 0 = 0.
@@ -44,6 +43,7 @@ Qed.
 
 
 (* Arithmetic *)
+Open Scope Z_scope.
 
 Goal 1 + 1 = 2.
 
@@ -221,4 +221,4 @@ Goal mrf (S (S O)) = true.
 
 zenon.
 
-*)
-\ No newline at end of file
+*)