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/FMapFacts.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/FMapFacts.v')
| -rw-r--r-- | theories/FSets/FMapFacts.v | 22 |
1 files changed, 11 insertions, 11 deletions
diff --git a/theories/FSets/FMapFacts.v b/theories/FSets/FMapFacts.v index 0e3b5cef1..083965cb7 100644 --- a/theories/FSets/FMapFacts.v +++ b/theories/FSets/FMapFacts.v @@ -702,18 +702,18 @@ Add Parametric Morphism elt : (@add elt) with signature E.eq ==> eq ==> Equal ==> Equal as add_m. Proof. intros k k' Hk e m m' Hm y. -rewrite add_o, add_o; do 2 destruct eq_dec; auto. -elim n; rewrite <-Hk; auto. -elim n; rewrite Hk; auto. +rewrite add_o, add_o; do 2 destruct eq_dec as [|?Hnot]; auto. +elim Hnot; rewrite <-Hk; auto. +elim Hnot; rewrite Hk; auto. Qed. Add Parametric Morphism elt : (@remove elt) with signature E.eq ==> Equal ==> Equal as remove_m. Proof. intros k k' Hk m m' Hm y. -rewrite remove_o, remove_o; do 2 destruct eq_dec; auto. -elim n; rewrite <-Hk; auto. -elim n; rewrite Hk; auto. +rewrite remove_o, remove_o; do 2 destruct eq_dec as [|?Hnot]; auto. +elim Hnot; rewrite <-Hk; auto. +elim Hnot; rewrite Hk; auto. Qed. Add Parametric Morphism elt elt' : (@map elt elt') @@ -861,7 +861,7 @@ Module WProperties_fun (E:DecidableType)(M:WSfun E). inversion_clear Hnodup as [| ? ? Hnotin Hnodup']. specialize (IH k Hnodup'); clear Hnodup'. rewrite add_o, IH. - unfold eqb; do 2 destruct eq_dec; auto; elim n; eauto. + unfold eqb; do 2 destruct eq_dec as [|?Hnot]; auto; elim Hnot; eauto. Qed. Lemma of_list_2 : forall l, NoDupA eqk l -> @@ -928,7 +928,7 @@ Module WProperties_fun (E:DecidableType)(M:WSfun E). apply InA_eqke_eqk with k e'; auto. rewrite <- of_list_1; auto. intro k'. rewrite Hsame, add_o, of_list_1b. simpl. - unfold eqb. do 2 destruct eq_dec; auto; elim n; eauto. + unfold eqb. do 2 destruct eq_dec as [|?Hnot]; auto; elim Hnot; eauto. inversion_clear Hdup; auto. apply IHl. intros; eapply Hstep'; eauto. @@ -1890,7 +1890,7 @@ Module OrdProperties (M:S). find_mapsto_iff, (H0 t0), <- find_mapsto_iff, add_mapsto_iff by (auto with *). unfold O.eqke; simpl. intuition. - destruct (E.eq_dec x t0); auto. + destruct (E.eq_dec x t0) as [Heq|Hneq]; auto. exfalso. assert (In t0 m). exists e0; auto. @@ -1919,7 +1919,7 @@ Module OrdProperties (M:S). find_mapsto_iff, (H0 t0), <- find_mapsto_iff, add_mapsto_iff by (auto with *). unfold O.eqke; simpl. intuition. - destruct (E.eq_dec x t0); auto. + destruct (E.eq_dec x t0) as [Heq|Hneq]; auto. exfalso. assert (In t0 m). exists e0; auto. @@ -1975,7 +1975,7 @@ Module OrdProperties (M:S). inversion_clear H1; [ | inversion_clear H2; eauto ]. red in H3; simpl in H3; destruct H3. destruct p as (p1,p2). - destruct (E.eq_dec p1 x). + destruct (E.eq_dec p1 x) as [Heq|Hneq]. apply ME.lt_eq with p1; auto. inversion_clear H2. inversion_clear H5. |