diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2014-06-01 10:26:26 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2014-06-01 11:33:55 +0200 |
| commit | 76adb57c72fccb4f3e416bd7f3927f4fff72178b (patch) | |
| tree | f8d72073a2ea62d3e5c274c201ef06532ac57b61 /theories/FSets/FMapAVL.v | |
| parent | be01deca2b8ff22505adaa66f55f005673bf2d85 (diff) | |
Making those proofs which depend on names generated for the arguments
in Prop of constructors of inductive types independent of these names.
Incidentally upgraded/simplified a couple of proofs, mainly in Reals.
This prepares to the next commit about using names based on H for such
hypotheses in Prop.
Diffstat (limited to 'theories/FSets/FMapAVL.v')
| -rw-r--r-- | theories/FSets/FMapAVL.v | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/theories/FSets/FMapAVL.v b/theories/FSets/FMapAVL.v index bee922c6f..7f5853494 100644 --- a/theories/FSets/FMapAVL.v +++ b/theories/FSets/FMapAVL.v @@ -1270,10 +1270,10 @@ Proof. inv bst. rewrite H2, join_find; auto; clear H2. - simpl; destruct X.compare; simpl; auto. + simpl; destruct X.compare as [Hlt| |Hlt]; simpl; auto. destruct (find y m2'); auto. symmetry; rewrite not_find_iff; auto; intro. - apply (MX.lt_not_gt l); apply H1; auto; rewrite H3; auto. + apply (MX.lt_not_gt Hlt); apply H1; auto; rewrite H3; auto. intros z Hz; apply H1; auto; rewrite H3; auto. Qed. @@ -1622,8 +1622,8 @@ Lemma map_option_find : forall (m:t elt)(x:key), Proof. intros m; functional induction (map_option f m); simpl; auto; intros; inv bst; rewrite join_find || rewrite concat_find; auto; simpl; - try destruct X.compare; simpl; auto. -rewrite (f_compat d e); auto. + try destruct X.compare as [Hlt|Heq|Hlt]; simpl; auto. +rewrite (f_compat d Heq); auto. intros y H; destruct (map_option_2 H) as (? & ? & ?); eauto using MapsTo_In. intros y H; @@ -1631,7 +1631,7 @@ intros y H; rewrite <- IHt, IHt0; auto; nonify (find x0 r); auto. rewrite IHt, IHt0; auto; nonify (find x0 r); nonify (find x0 l); auto. -rewrite (f_compat d e); auto. +rewrite (f_compat d Heq); auto. rewrite <- IHt0, IHt; auto; nonify (find x0 l); auto. destruct (find x0 (map_option f r)); auto. |