diff options
author | Enrico Tassi <gareuselesinge@debian.org> | 2015-01-25 14:42:51 +0100 |
---|---|---|
committer | Enrico Tassi <gareuselesinge@debian.org> | 2015-01-25 14:42:51 +0100 |
commit | 7cfc4e5146be5666419451bdd516f1f3f264d24a (patch) | |
tree | e4197645da03dc3c7cc84e434cc31d0a0cca7056 /theories/FSets/FSetBridge.v | |
parent | 420f78b2caeaaddc6fe484565b2d0e49c66888e5 (diff) |
Imported Upstream version 8.5~beta1+dfsg
Diffstat (limited to 'theories/FSets/FSetBridge.v')
-rw-r--r-- | theories/FSets/FSetBridge.v | 20 |
1 files changed, 10 insertions, 10 deletions
diff --git a/theories/FSets/FSetBridge.v b/theories/FSets/FSetBridge.v index 1ac544e1..97f140b3 100644 --- a/theories/FSets/FSetBridge.v +++ b/theories/FSets/FSetBridge.v @@ -284,7 +284,7 @@ Module DepOfNodep (Import M: S) <: Sdep with Module E := M.E. Lemma choose_equal : forall s s', Equal s s' -> match choose s, choose s' with - | inleft (exist x _), inleft (exist x' _) => E.eq x x' + | inleft (exist _ x _), inleft (exist _ x' _) => E.eq x x' | inright _, inright _ => True | _, _ => False end. @@ -423,7 +423,7 @@ Module NodepOfDep (M: Sdep) <: S with Module E := M.E. Definition choose (s : t) : option elt := match choose s with - | inleft (exist x _) => Some x + | inleft (exist _ x _) => Some x | inright _ => None end. @@ -472,7 +472,7 @@ Module NodepOfDep (M: Sdep) <: S with Module E := M.E. Definition min_elt (s : t) : option elt := match min_elt s with - | inleft (exist x _) => Some x + | inleft (exist _ x _) => Some x | inright _ => None end. @@ -500,7 +500,7 @@ Module NodepOfDep (M: Sdep) <: S with Module E := M.E. Definition max_elt (s : t) : option elt := match max_elt s with - | inleft (exist x _) => Some x + | inleft (exist _ x _) => Some x | inright _ => None end. @@ -673,24 +673,24 @@ Module NodepOfDep (M: Sdep) <: S with Module E := M.E. forall (s : t) (x : elt) (f : elt -> bool), compat_bool E.eq f -> In x (filter f s) -> In x s. Proof. - intros s x f; unfold filter; case M.filter; intuition. - generalize (i (compat_P_aux H)); firstorder. + intros s x f; unfold filter; case M.filter as (x0,Hiff); intuition. + generalize (Hiff (compat_P_aux H)); firstorder. Qed. Lemma filter_2 : forall (s : t) (x : elt) (f : elt -> bool), compat_bool E.eq f -> In x (filter f s) -> f x = true. Proof. - intros s x f; unfold filter; case M.filter; intuition. - generalize (i (compat_P_aux H)); firstorder. + intros s x f; unfold filter; case M.filter as (x0,Hiff); intuition. + generalize (Hiff (compat_P_aux H)); firstorder. Qed. Lemma filter_3 : forall (s : t) (x : elt) (f : elt -> bool), compat_bool E.eq f -> In x s -> f x = true -> In x (filter f s). Proof. - intros s x f; unfold filter; case M.filter; intuition. - generalize (i (compat_P_aux H)); firstorder. + intros s x f; unfold filter; case M.filter as (x0,Hiff); intuition. + generalize (Hiff (compat_P_aux H)); firstorder. Qed. Definition for_all (f : elt -> bool) (s : t) : bool := |