summaryrefslogtreecommitdiff
path: root/theories/FSets/FMapList.v
diff options
context:
space:
mode:
authorGravatar Samuel Mimram <smimram@debian.org>2006-07-13 14:28:31 +0000
committerGravatar Samuel Mimram <smimram@debian.org>2006-07-13 14:28:31 +0000
commitde0085539583f59dc7c4bf4e272e18711d565466 (patch)
tree347e1d95a2df56f79a01b303e485563588179e91 /theories/FSets/FMapList.v
parente978da8c41d8a3c19a29036d9c569fbe2a4616b0 (diff)
Imported Upstream version 8.0pl3+8.1beta.2upstream/8.0pl3+8.1beta.2
Diffstat (limited to 'theories/FSets/FMapList.v')
-rw-r--r--theories/FSets/FMapList.v42
1 files changed, 20 insertions, 22 deletions
diff --git a/theories/FSets/FMapList.v b/theories/FSets/FMapList.v
index c671ba82..067f5a3e 100644
--- a/theories/FSets/FMapList.v
+++ b/theories/FSets/FMapList.v
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(***********************************************************************)
-(* $Id: FMapList.v 8899 2006-06-06 11:09:43Z jforest $ *)
+(* $Id: FMapList.v 9035 2006-07-09 15:42:09Z herbelin $ *)
(** * Finite map library *)
@@ -20,8 +20,6 @@ Require Import FMapInterface.
Set Implicit Arguments.
Unset Strict Implicit.
-Arguments Scope list [type_scope].
-
Module Raw (X:OrderedType).
Module E := X.
@@ -161,14 +159,14 @@ Proof.
inversion 2.
inversion_clear 2.
- clear H0;compute in H1; destruct H1;order.
- clear H0;generalize (Sort_In_cons_1 Hm (InA_eqke_eqk H1)); compute; order.
+ clear e1;compute in H0; destruct H0;order.
+ clear e1;generalize (Sort_In_cons_1 Hm (InA_eqke_eqk H0)); compute; order.
- clear H0;inversion_clear 2.
+ clear e1;inversion_clear 2.
compute in H0; destruct H0; intuition congruence.
generalize (Sort_In_cons_1 Hm (InA_eqke_eqk H0)); compute; order.
- clear H0; do 2 inversion_clear 1; auto.
+ clear e1; do 2 inversion_clear 1; auto.
compute in H2; destruct H2; order.
Qed.
@@ -197,7 +195,7 @@ Lemma add_2 : forall m x y e e',
Proof.
intros m x y e e'.
generalize y e; clear y e; unfold PX.MapsTo.
- functional induction (add x e' m) ;simpl;auto; clear H0.
+ functional induction (add x e' m) ;simpl;auto; clear e0.
subst;auto.
intros y' e'' eqky'; inversion_clear 1; destruct H0; simpl in *.
@@ -214,9 +212,9 @@ Proof.
intros m x y e e'. generalize y e; clear y e; unfold PX.MapsTo.
functional induction (add x e' m);simpl; intros.
apply (In_inv_3 H0); compute; auto.
- apply (In_inv_3 H1); compute; auto.
- constructor 2; apply (In_inv_3 H1); compute; auto.
- inversion_clear H1; auto.
+ apply (In_inv_3 H0); compute; auto.
+ constructor 2; apply (In_inv_3 H0); compute; auto.
+ inversion_clear H0; auto.
Qed.
@@ -265,13 +263,13 @@ Proof.
red; inversion 1; inversion H1.
apply Sort_Inf_NotIn with x0; auto.
- clear H0;constructor; compute; order.
+ clear e0;constructor; compute; order.
- clear H0;inversion_clear Hm.
+ clear e0;inversion_clear Hm.
apply Sort_Inf_NotIn with x0; auto.
apply Inf_eq with (k',x0);auto; compute; apply X.eq_trans with x; auto.
- clear H0;inversion_clear Hm.
+ clear e0;inversion_clear Hm.
assert (notin:~ In y (remove x l)) by auto.
intros (x1,abs).
inversion_clear abs.
@@ -393,7 +391,7 @@ Proof.
assert (cmp_e_e':cmp e e' = true).
- apply H2 with x; auto.
+ apply H1 with x; auto.
rewrite cmp_e_e'; simpl.
apply IHb; auto.
inversion_clear Hm; auto.
@@ -402,7 +400,7 @@ Proof.
destruct (H0 k).
assert (In k ((x,e) ::l)).
destruct H as (e'', hyp); exists e''; auto.
- destruct (In_inv (H1 H4)); auto.
+ destruct (In_inv (H2 H4)); auto.
inversion_clear Hm.
elim (Sort_Inf_NotIn H6 H7).
destruct H as (e'', hyp); exists e''; auto.
@@ -415,10 +413,10 @@ Proof.
elim (Sort_Inf_NotIn H6 H7).
destruct H as (e'', hyp); exists e''; auto.
apply MapsTo_eq with k; auto; order.
- apply H2 with k; destruct (eq_dec x k); auto.
+ apply H1 with k; destruct (eq_dec x k); auto.
- destruct (X.compare x x'); try contradiction;clear H2.
+ destruct (X.compare x x'); try contradiction; clear y.
destruct (H0 x).
assert (In x ((x',e')::l')).
apply H; auto.
@@ -492,16 +490,16 @@ Proof.
inversion_clear Hm;inversion_clear Hm'.
destruct (andb_prop _ _ H); clear H.
- destruct (IHb H1 H4 H7).
+ destruct (IHb H2 H4 H7).
inversion_clear H0.
destruct H9; simpl in *; subst.
- inversion_clear H2.
+ inversion_clear H1.
destruct H9; simpl in *; subst; auto.
elim (Sort_Inf_NotIn H4 H5).
exists e'0; apply MapsTo_eq with k; auto; order.
- inversion_clear H2.
+ inversion_clear H1.
destruct H0; simpl in *; subst; auto.
- elim (Sort_Inf_NotIn H1 H3).
+ elim (Sort_Inf_NotIn H2 H3).
exists e0; apply MapsTo_eq with k; auto; order.
apply H8 with k; auto.
Qed.