diff options
Diffstat (limited to 'theories')
| -rw-r--r-- | theories/Arith/Compare_dec.v | 4 | ||||
| -rw-r--r-- | theories/Arith/Peano_dec.v | 4 | ||||
| -rw-r--r-- | theories/FSets/FMapAVL.v | 8 | ||||
| -rw-r--r-- | theories/FSets/FMapPositive.v | 4 | ||||
| -rw-r--r-- | theories/FSets/FSetAVL.v | 6 | ||||
| -rw-r--r-- | theories/FSets/OrderedTypeEx.v | 10 | ||||
| -rw-r--r-- | theories/QArith/QArith_base.v | 6 | ||||
| -rw-r--r-- | theories/ZArith/ZArith_dec.v | 4 |
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. |