Imported Upstream version 8.1.pl1+dfsgupstream/8.1.pl1+dfsg

8 files changed, 23 insertions, 23 deletions

diff --git a/theories/Arith/Compare_dec.v b/theories/Arith/Compare_dec.v
index e6dc7c46..b431fd05 100644
--- a/theories/Arith/Compare_dec.v
+++ b/theories/Arith/Compare_dec.v
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: Compare_dec.v 9245 2006-10-17 12:53:34Z notin $ i*)
+(*i $Id: Compare_dec.v 9941 2007-07-05 12:42:35Z letouzey $ i*)
 
 Require Import Le.
 Require Import Lt.
@@ -34,7 +34,7 @@ Defined.
 Definition le_lt_dec n m : {n <= m} + {m < n}.
   induction n.
   auto with arith.
-  induction m.
+  destruct m.
   auto with arith.
   elim (IHn m); auto with arith.
 Defined.
diff --git a/theories/Arith/Peano_dec.v b/theories/Arith/Peano_dec.v
index b17021bc..9ae80d79 100644
--- a/theories/Arith/Peano_dec.v
+++ b/theories/Arith/Peano_dec.v
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: Peano_dec.v 9245 2006-10-17 12:53:34Z notin $ i*)
+(*i $Id: Peano_dec.v 9941 2007-07-05 12:42:35Z letouzey $ i*)
 
 Require Import Decidable.
 
@@ -23,7 +23,7 @@ Defined.
 
 Theorem eq_nat_dec : forall n m, {n = m} + {n <> m}.
 Proof.
-  induction n; induction m; auto.
+  induction n; destruct m; auto.
   elim (IHn m); auto.
 Defined.
 
diff --git a/theories/FSets/FMapAVL.v b/theories/FSets/FMapAVL.v
index 786ade0e..4807ed66 100644
--- a/theories/FSets/FMapAVL.v
+++ b/theories/FSets/FMapAVL.v
@@ -9,7 +9,7 @@
 
 (* Finite map library.  *)
 
-(* $Id: FMapAVL.v 8985 2006-06-23 16:12:45Z jforest $ *)
+(* $Id: FMapAVL.v 9862 2007-05-25 16:57:06Z letouzey $ *)
 
 (** This module implements map using AVL trees.
     It follows the implementation from Ocaml's standard library. *)
@@ -30,7 +30,7 @@ Module Raw (I:Int)(X: OrderedType).
 Import I.
 Module II:=MoreInt(I).
 Import II.
-Open Scope Int_scope.
+Open Local Scope Int_scope.
 
 Module E := X.
 Module MX := OrderedTypeFacts X.
@@ -1229,7 +1229,7 @@ Proof.
  apply compare_flatten_1.
 Qed.
 
-Open Scope Z_scope.
+Open Local Scope Z_scope.
 
 (** termination of [compare_aux] *)
  
@@ -1967,7 +1967,7 @@ Module IntMake_ord (I:Int)(X: OrderedType)(D : OrderedType) <:
   Definition flatten_slist (e:enumeration D.t)(He:sorted_e e) := 
    LO.MapS.Build_slist (sorted_flatten_e He). 
 
-  Open Scope Z_scope.
+  Open Local Scope Z_scope.
 
   Definition compare_aux : 
    forall (e1 e2:enumeration D.t)(He1:sorted_e e1)(He2: sorted_e e2), 
diff --git a/theories/FSets/FMapPositive.v b/theories/FSets/FMapPositive.v
index 911de00e..44724767 100644
--- a/theories/FSets/FMapPositive.v
+++ b/theories/FSets/FMapPositive.v
@@ -11,7 +11,7 @@
  * Institution: LRI, CNRS UMR 8623 - Université Paris Sud
  *              91405 Orsay, France *)
 
-(* $Id: FMapPositive.v 9178 2006-09-26 11:18:22Z barras $ *)
+(* $Id: FMapPositive.v 9862 2007-05-25 16:57:06Z letouzey $ *)
 
 Require Import Bool.
 Require Import ZArith.
@@ -20,7 +20,7 @@ Require Import FMapInterface.
 
 Set Implicit Arguments.
 
-Open Scope positive_scope.
+Open Local Scope positive_scope.
 
 (** * An implementation of [FMapInterface.S] for positive keys. *)
 
diff --git a/theories/FSets/FSetAVL.v b/theories/FSets/FSetAVL.v
index 5b09945b..d5ce54d9 100644
--- a/theories/FSets/FSetAVL.v
+++ b/theories/FSets/FSetAVL.v
@@ -12,7 +12,7 @@
  * Institution: LRI, CNRS UMR 8623 - Université Paris Sud
  *              91405 Orsay, France *)
 
-(* $Id: FSetAVL.v 8985 2006-06-23 16:12:45Z jforest $ *)
+(* $Id: FSetAVL.v 9862 2007-05-25 16:57:06Z letouzey $ *)
 
 (** This module implements sets using AVL trees.
     It follows the implementation from Ocaml's standard library. *)
@@ -28,7 +28,7 @@ Module Raw (I:Int)(X:OrderedType).
 Import I.
 Module II:=MoreInt(I).
 Import II.
-Open Scope Int_scope.
+Open Local Scope Int_scope.
 
 Module E := X.
 Module MX := OrderedTypeFacts X.
@@ -2286,7 +2286,7 @@ Qed.
 
 (** termination of [compare_aux] *)
 
-Open Scope Z_scope.
+Open Local Scope Z_scope.
  
 Fixpoint measure_e_t (s : tree) : Z := match s with
   | Leaf => 0
diff --git a/theories/FSets/OrderedTypeEx.v b/theories/FSets/OrderedTypeEx.v
index 6fa6a85c..28a5705d 100644
--- a/theories/FSets/OrderedTypeEx.v
+++ b/theories/FSets/OrderedTypeEx.v
@@ -11,7 +11,7 @@
  * Institution: LRI, CNRS UMR 8623 - Université Paris Sud
  *              91405 Orsay, France *)
 
-(* $Id: OrderedTypeEx.v 9066 2006-08-14 10:11:18Z letouzey $ *)
+(* $Id: OrderedTypeEx.v 9940 2007-07-05 12:32:47Z letouzey $ *)
 
 Require Import OrderedType.
 Require Import ZArith.
@@ -73,7 +73,7 @@ End Nat_as_OT.
 
 (** [Z] is an ordered type with respect to the usual order on integers. *)
 
-Open Scope Z_scope.
+Open Local Scope Z_scope.
 
 Module Z_as_OT <: UsualOrderedType.
 
@@ -103,7 +103,7 @@ End Z_as_OT.
 
 (** [positive] is an ordered type with respect to the usual order on natural numbers. *) 
 
-Open Scope positive_scope.
+Open Local Scope positive_scope.
 
 Module Positive_as_OT <: UsualOrderedType.
   Definition t:=positive.
@@ -138,14 +138,14 @@ Module Positive_as_OT <: UsualOrderedType.
   apply GT; unfold lt.
   replace Eq with (CompOpp Eq); auto.
   rewrite <- Pcompare_antisym; rewrite H; auto.
-  Qed.
+  Defined.
 
 End Positive_as_OT.
 
 
 (** [N] is an ordered type with respect to the usual order on natural numbers. *) 
 
-Open Scope positive_scope.
+Open Local Scope positive_scope.
 
 Module N_as_OT <: UsualOrderedType.
   Definition t:=N.
diff --git a/theories/QArith/QArith_base.v b/theories/QArith/QArith_base.v
index 66d16cfe..fc92c678 100644
--- a/theories/QArith/QArith_base.v
+++ b/theories/QArith/QArith_base.v
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: QArith_base.v 9245 2006-10-17 12:53:34Z notin $ i*)
+(*i $Id: QArith_base.v 9932 2007-07-02 14:31:33Z notin $ i*)
 
 Require Export ZArith.
 Require Export ZArithRing.
@@ -38,8 +38,8 @@ Notation " 1 " := (1#1) : Q_scope.
 Definition Qeq (p q : Q) := (Qnum p * QDen q)%Z = (Qnum q * QDen p)%Z.
 Definition Qle (x y : Q) := (Qnum x * QDen y <= Qnum y * QDen x)%Z.
 Definition Qlt (x y : Q) := (Qnum x * QDen y < Qnum y * QDen x)%Z.
-Notation Qgt := (fun x y : Q => Qlt y x).
-Notation Qge := (fun x y : Q => Qle y x).
+Notation Qgt := (fun a b : Q => Qlt b a).
+Notation Qge := (fun a b : Q => Qle b a).
 
 Infix "==" := Qeq (at level 70, no associativity) : Q_scope. 
 Infix "<" := Qlt : Q_scope.
diff --git a/theories/ZArith/ZArith_dec.v b/theories/ZArith/ZArith_dec.v
index 84249955..7febbf6a 100644
--- a/theories/ZArith/ZArith_dec.v
+++ b/theories/ZArith/ZArith_dec.v
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: ZArith_dec.v 9245 2006-10-17 12:53:34Z notin $ i*)
+(*i $Id: ZArith_dec.v 9958 2007-07-06 22:47:40Z letouzey $ i*)
 
 Require Import Sumbool.
 
@@ -94,7 +94,7 @@ Section decidability.
     elim Z_lt_ge_dec.
     intros; left; assumption.
     intros; right; apply Zge_le; assumption.
-  Qed.
+  Defined.
 
   Definition Z_le_gt_dec : {x <= y} + {x > y}.
   Proof.