summaryrefslogtreecommitdiff
path: root/theories
diff options
context:
space:
mode:
Diffstat (limited to 'theories')
-rw-r--r--theories/Arith/Compare_dec.v4
-rw-r--r--theories/Arith/Peano_dec.v4
-rw-r--r--theories/FSets/FMapAVL.v8
-rw-r--r--theories/FSets/FMapPositive.v4
-rw-r--r--theories/FSets/FSetAVL.v6
-rw-r--r--theories/FSets/OrderedTypeEx.v10
-rw-r--r--theories/QArith/QArith_base.v6
-rw-r--r--theories/ZArith/ZArith_dec.v4
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.