diff options
| author | Théo Zimmermann | 2019-04-03 10:00:17 +0200 |
|---|---|---|
| committer | Théo Zimmermann | 2019-04-03 10:00:17 +0200 |
| commit | 8f37727a0cb99eb7f250bd507635de6628de23ad (patch) | |
| tree | 0f381cf21c103be423eea4a6bf7570db5d38d15f /theories/FSets | |
| parent | a675df0fc21ce00f120046619751656eabcdbaed (diff) | |
| parent | b1162463d577baf450c3f33ab880e7d9afe21148 (diff) | |
Merge PR #8638: Remove -compat 8.7
Reviewed-by: Zimmi48
Reviewed-by: ejgallego
Reviewed-by: jfehrle
Ack-by: maximedenes
Reviewed-by: ppedrot
Diffstat (limited to 'theories/FSets')
| -rw-r--r-- | theories/FSets/FMapFacts.v | 7 |
1 files changed, 2 insertions, 5 deletions
diff --git a/theories/FSets/FMapFacts.v b/theories/FSets/FMapFacts.v index d19c5558d8..e68bc5930d 100644 --- a/theories/FSets/FMapFacts.v +++ b/theories/FSets/FMapFacts.v @@ -26,8 +26,6 @@ Hint Extern 1 (Equivalence _) => constructor; congruence : core. Module WFacts_fun (E:DecidableType)(Import M:WSfun E). -Notation option_map := option_map (compat "8.7"). - Notation eq_dec := E.eq_dec. Definition eqb x y := if eq_dec x y then true else false. @@ -676,7 +674,7 @@ Qed. Add Parametric Morphism elt : (@Empty elt) with signature Equal ==> iff as Empty_m. Proof. -unfold Empty; intros m m' Hm. split; intros; intro. +unfold Empty; intros m m' Hm. split; intros; intro. rewrite <-Hm in H0; eapply H, H0. rewrite Hm in H0; eapply H, H0. Qed. @@ -758,7 +756,7 @@ Module WProperties_fun (E:DecidableType)(M:WSfun E). Instance eqk_equiv : Equivalence eqk. Proof. unfold eq_key; split; eauto. Qed. - + Instance eqke_equiv : Equivalence eqke. Proof. unfold eq_key_elt; split; repeat red; firstorder. @@ -2198,4 +2196,3 @@ Module OrdProperties (M:S). End Elt. End OrdProperties. - |