diff options
author | 2008-02-05 16:31:16 +0000 | |
---|---|---|
committer | 2008-02-05 16:31:16 +0000 | |
commit | 316e114dd188f85ec657420989bf909ecfe9d006 (patch) | |
tree | 37229712b18593049740b28b6a18a5d9e7150faa /theories | |
parent | 44cedab7be5a44a01d467fbd2dba24400d575206 (diff) |
kill some useless module aliases E:=X (for better name printing, see Elie's 14097)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10511 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories')
-rw-r--r-- | theories/FSets/FMapAVL.v | 1 | ||||
-rw-r--r-- | theories/FSets/FMapList.v | 1 | ||||
-rw-r--r-- | theories/FSets/FMapWeakList.v | 2 | ||||
-rw-r--r-- | theories/FSets/FSetAVL.v | 9 | ||||
-rw-r--r-- | theories/FSets/FSetList.v | 3 | ||||
-rw-r--r-- | theories/FSets/FSetWeakList.v | 2 |
6 files changed, 6 insertions, 12 deletions
diff --git a/theories/FSets/FMapAVL.v b/theories/FSets/FMapAVL.v index 0e9bd6e5e..0652f7491 100644 --- a/theories/FSets/FMapAVL.v +++ b/theories/FSets/FMapAVL.v @@ -32,7 +32,6 @@ Module II:=MoreInt(I). Import II. Open Local Scope Int_scope. -Module E := X. Module MX := OrderedTypeFacts X. Module PX := KeyOrderedType X. Module L := FMapList.Raw X. diff --git a/theories/FSets/FMapList.v b/theories/FSets/FMapList.v index b86e558b3..dfe842730 100644 --- a/theories/FSets/FMapList.v +++ b/theories/FSets/FMapList.v @@ -21,7 +21,6 @@ Unset Strict Implicit. Module Raw (X:OrderedType). -Module E := X. Module Import MX := OrderedTypeFacts X. Module Import PX := KeyOrderedType X. diff --git a/theories/FSets/FMapWeakList.v b/theories/FSets/FMapWeakList.v index 579fd50c9..0dcfb05f3 100644 --- a/theories/FSets/FMapWeakList.v +++ b/theories/FSets/FMapWeakList.v @@ -11,7 +11,7 @@ (** * Finite map library *) (** This file proposes an implementation of the non-dependant interface - [FMapInterface.WS] using lists of pairs, unordered but without redundancy. *) + [FMapInterface.WS] using lists of pairs, unordered but without redundancy. *) Require Import FMapInterface. diff --git a/theories/FSets/FSetAVL.v b/theories/FSets/FSetAVL.v index 20fdae9fe..b6bcb6fb4 100644 --- a/theories/FSets/FSetAVL.v +++ b/theories/FSets/FSetAVL.v @@ -30,7 +30,6 @@ Module II:=MoreInt(I). Import II. Open Local Scope Int_scope. -Module E := X. Module MX := OrderedTypeFacts X. Definition elt := X.t. @@ -1647,7 +1646,7 @@ Fixpoint for_all (s:t) : bool := match s with | Node l x r _ => f x && for_all l && for_all r end. -Lemma for_all_1 : forall s, compat_bool E.eq f -> +Lemma for_all_1 : forall s, compat_bool X.eq f -> For_all (fun x => f x = true) s -> for_all s = true. Proof. induction s; simpl; auto. @@ -1658,7 +1657,7 @@ Proof. destruct (f t); simpl; auto. Qed. -Lemma for_all_2 : forall s, compat_bool E.eq f -> +Lemma for_all_2 : forall s, compat_bool X.eq f -> for_all s = true -> For_all (fun x => f x = true) s. Proof. induction s; simpl; auto; intros; red; intros; inv In. @@ -1676,7 +1675,7 @@ Fixpoint exists_ (s:t) : bool := match s with | Node l x r _ => f x || exists_ l || exists_ r end. -Lemma exists_1 : forall s, compat_bool E.eq f -> +Lemma exists_1 : forall s, compat_bool X.eq f -> Exists (fun x => f x = true) s -> exists_ s = true. Proof. induction s; simpl; destruct 2 as (x,(U,V)); inv In. @@ -1686,7 +1685,7 @@ Proof. apply orb_true_intro; right; apply IHs2; firstorder. Qed. -Lemma exists_2 : forall s, compat_bool E.eq f -> +Lemma exists_2 : forall s, compat_bool X.eq f -> exists_ s = true -> Exists (fun x => f x = true) s. Proof. induction s; simpl; intros. diff --git a/theories/FSets/FSetList.v b/theories/FSets/FSetList.v index 4393c67f7..322e970cf 100644 --- a/theories/FSets/FSetList.v +++ b/theories/FSets/FSetList.v @@ -25,7 +25,6 @@ Unset Strict Implicit. Module Raw (X: OrderedType). - Module E := X. Module MX := OrderedTypeFacts X. Import MX. @@ -649,7 +648,7 @@ Module Raw (X: OrderedType). unfold elements; auto. Qed. - Lemma elements_3w : forall (s : t) (Hs : Sort s), NoDupA E.eq (elements s). + Lemma elements_3w : forall (s : t) (Hs : Sort s), NoDupA X.eq (elements s). Proof. unfold elements; auto. Qed. diff --git a/theories/FSets/FSetWeakList.v b/theories/FSets/FSetWeakList.v index c692950e0..3039c058c 100644 --- a/theories/FSets/FSetWeakList.v +++ b/theories/FSets/FSetWeakList.v @@ -24,8 +24,6 @@ Unset Strict Implicit. And the functions returning sets are proved to preserve this invariant. *) Module Raw (X: DecidableType). - - Module E := X. Definition elt := X.t. Definition t := list elt. |