From d4c5a863d35bb131b7236fd5df48cfc882c0b0f1 Mon Sep 17 00:00:00 2001
From: herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7>
Date: Mon, 2 May 2005 10:46:25 +0000
Subject: Utilisation Z_scope

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6982 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 contrib7/omega/OmegaLemmas.v | 2 ++
 1 file changed, 2 insertions(+)

(limited to 'contrib7')

diff --git a/contrib7/omega/OmegaLemmas.v b/contrib7/omega/OmegaLemmas.v
index f9027d348..b27afd0dd 100644
--- a/contrib7/omega/OmegaLemmas.v
+++ b/contrib7/omega/OmegaLemmas.v
@@ -10,6 +10,8 @@
 
 Require ZArith_base.
 
+Open Scope Z_scope.
+
 (** These are specific variants of theorems dedicated for the Omega tactic *)
 
 Lemma new_var: (x:Z) (EX y:Z |(x=y)).
-- 
cgit v1.2.3