diff options
| author | Jason Gross | 2018-10-02 16:14:20 -0400 |
|---|---|---|
| committer | Vincent Laporte | 2019-04-02 11:55:51 +0000 |
| commit | b1162463d577baf450c3f33ab880e7d9afe21148 (patch) | |
| tree | d85438c47e85ebda6cbccab94daf5d312c502e44 /theories/FSets | |
| parent | 974dc811fe30a762235b68fb3c0ac5c3eeca45b9 (diff) | |
Remove -compat 8.7
This removes various compatibility notations.
Closes #8374
This commit was mostly created by running `./dev/tools/update-compat.py
--release`. There's a bit of manual spacing adjustment around all of the
removed compatibility notations, and some test-suite updates were done
manually.
The update to CHANGES.md was manual.
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. - |