*** empty log message ***

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3761 85f007b7-540e-0410-9357-904b9bb8a0f7

18 files changed, 20 insertions, 0 deletions

diff --git a/theories/Arith/Between.v b/theories/Arith/Between.v
index 112edaa566..5711a81a74 100755
--- a/theories/Arith/Between.v
+++ b/theories/Arith/Between.v
@@ -10,6 +10,7 @@
 
 Require Le.
 Require Lt.
+Import nat_scope.
 
 Section Between.
 Variables P,Q : nat -> Prop.
diff --git a/theories/Arith/Bool_nat.v b/theories/Arith/Bool_nat.v
index 872c314f16..bbe1475f50 100644
--- a/theories/Arith/Bool_nat.v
+++ b/theories/Arith/Bool_nat.v
@@ -11,6 +11,7 @@
 Require Export Compare_dec.
 Require Export Peano_dec.
 Require Sumbool.
+Import nat_scope.
 
 (** The decidability of equality and order relations over
     type [nat] give some boolean functions with the adequate specification. *)
diff --git a/theories/Arith/Compare.v b/theories/Arith/Compare.v
index f98115e6b7..5b12033dc7 100755
--- a/theories/Arith/Compare.v
+++ b/theories/Arith/Compare.v
@@ -9,6 +9,7 @@
 (*i $Id$ i*)
 
 (** Equality is decidable on [nat] *)
+Import nat_scope.
 
 Lemma not_eq_sym : (A:Set)(p,q:A)(~p=q) -> ~(q=p).
 Proof sym_not_eq.
diff --git a/theories/Arith/Compare_dec.v b/theories/Arith/Compare_dec.v
index 67218de837..735d267d64 100755
--- a/theories/Arith/Compare_dec.v
+++ b/theories/Arith/Compare_dec.v
@@ -12,6 +12,7 @@ Require Le.
 Require Lt.
 Require Gt.
 Require Decidable.
+Import nat_scope.
 
 Definition zerop : (n:nat){n=O}+{lt O n}.
 NewDestruct n; Auto with arith.
diff --git a/theories/Arith/Div.v b/theories/Arith/Div.v
index 2b7cfac144..e4b0300dd7 100755
--- a/theories/Arith/Div.v
+++ b/theories/Arith/Div.v
@@ -9,6 +9,7 @@
 (*i $Id$ i*)
 
 (** Euclidean division *)
+Import nat_scope.
 
 Require Le.
 Require Euclid_def.
diff --git a/theories/Arith/Div2.v b/theories/Arith/Div2.v
index f039aa7a0d..dd0cc84583 100644
--- a/theories/Arith/Div2.v
+++ b/theories/Arith/Div2.v
@@ -12,6 +12,7 @@ Require Lt.
 Require Plus.
 Require Compare_dec.
 Require Even.
+Import nat_scope.
 
 (** Here we define [n/2] and prove some of its properties *)
 
diff --git a/theories/Arith/EqNat.v b/theories/Arith/EqNat.v
index b4a232e204..88cca274b9 100755
--- a/theories/Arith/EqNat.v
+++ b/theories/Arith/EqNat.v
@@ -9,6 +9,7 @@
 (*i $Id$ i*)
 
 (** Equality on natural numbers *)
+Import nat_scope.
 
 Fixpoint  eq_nat [n:nat] : nat -> Prop :=
   [m:nat]Cases n m of 
diff --git a/theories/Arith/Euclid.v b/theories/Arith/Euclid.v
index 5a2dd1a84e..173a906387 100644
--- a/theories/Arith/Euclid.v
+++ b/theories/Arith/Euclid.v
@@ -11,6 +11,7 @@
 Require Mult.
 Require Compare_dec.
 Require Wf_nat.
+Import nat_scope.
 
 
 Inductive diveucl [a,b:nat] : Set 
diff --git a/theories/Arith/Even.v b/theories/Arith/Even.v
index 074e0a03d1..034a60088e 100644
--- a/theories/Arith/Even.v
+++ b/theories/Arith/Even.v
@@ -11,6 +11,7 @@
 (** Here we define the predicates [even] and [odd] by mutual induction
     and we prove the decidability and the exclusion of those predicates.
     The main results about parity are proved in the module Div2. *)
+Import nat_scope.
 
 Inductive even : nat->Prop :=
     even_O : (even O)
diff --git a/theories/Arith/Gt.v b/theories/Arith/Gt.v
index f31154018e..6b55c5bd3d 100755
--- a/theories/Arith/Gt.v
+++ b/theories/Arith/Gt.v
@@ -11,6 +11,7 @@
 Require Le.
 Require Lt.
 Require Plus.
+Import nat_scope.
 
 Theorem gt_Sn_O : (n:nat)(gt (S n) O).
 Proof.
diff --git a/theories/Arith/Le.v b/theories/Arith/Le.v
index 9bdb7dc239..7765187cf5 100755
--- a/theories/Arith/Le.v
+++ b/theories/Arith/Le.v
@@ -9,6 +9,8 @@
 (*i $Id$ i*)
 
 (** Order on natural numbers *)
+Import nat_scope.
+Open Scope nat_scope.
 
 Theorem le_n_S : (n,m:nat)(le n m)->(le (S n) (S m)).
 Proof.
diff --git a/theories/Arith/Lt.v b/theories/Arith/Lt.v
index 711e065da9..96541cb9f5 100755
--- a/theories/Arith/Lt.v
+++ b/theories/Arith/Lt.v
@@ -9,6 +9,7 @@
 (*i $Id$ i*)
 
 Require Le.
+Import nat_scope.
 
 Theorem lt_n_Sn : (n:nat)(lt n (S n)).
 Proof.
diff --git a/theories/Arith/Max.v b/theories/Arith/Max.v
index 43c683a908..8a599ed7ea 100755
--- a/theories/Arith/Max.v
+++ b/theories/Arith/Max.v
@@ -9,6 +9,7 @@
 (*i $Id$ i*)
 
 Require Arith.
+Import nat_scope.
 
 (** maximum of two natural numbers *)
 
diff --git a/theories/Arith/Min.v b/theories/Arith/Min.v
index 8a5de8703a..650b953803 100755
--- a/theories/Arith/Min.v
+++ b/theories/Arith/Min.v
@@ -9,6 +9,7 @@
 (*i $Id$ i*)
 
 Require Arith.
+Import nat_scope.
 
 (** minimum of two natural numbers *)
 
diff --git a/theories/Arith/Minus.v b/theories/Arith/Minus.v
index 0f435a5602..42f44083a8 100755
--- a/theories/Arith/Minus.v
+++ b/theories/Arith/Minus.v
@@ -12,6 +12,7 @@
 
 Require Lt.
 Require Le.
+Import nat_scope.
 
 Fixpoint minus [n:nat] : nat -> nat := 
   [m:nat]Cases n m of
diff --git a/theories/Arith/Mult.v b/theories/Arith/Mult.v
index ac16d4cb9f..1daf8567c2 100755
--- a/theories/Arith/Mult.v
+++ b/theories/Arith/Mult.v
@@ -11,6 +11,7 @@
 Require Export Plus.
 Require Export Minus.
 Require Export Lt.
+Import nat_scope.
 
 (** Multiplication *)
 
diff --git a/theories/Arith/Peano_dec.v b/theories/Arith/Peano_dec.v
index 694351b677..e998e0b7c0 100755
--- a/theories/Arith/Peano_dec.v
+++ b/theories/Arith/Peano_dec.v
@@ -9,6 +9,7 @@
 (*i $Id$ i*)
 
 Require Decidable.
+Import nat_scope.
 
 Theorem O_or_S : (n:nat)({m:nat|(S m)=n})+{O=n}.
 Proof.
diff --git a/theories/Arith/Wf_nat.v b/theories/Arith/Wf_nat.v
index 581b458515..b0c715c8bc 100755
--- a/theories/Arith/Wf_nat.v
+++ b/theories/Arith/Wf_nat.v
@@ -12,6 +12,8 @@
 
 Require Lt.
 
+Import nat_scope.
+
 Chapter  Well_founded_Nat.
 
 Variable A : Set.