diff options
| author | David Monniaux <David.Monniaux@univ-grenoble-alpes.fr> | 2021-10-29 21:56:59 +0200 |
|---|---|---|
| committer | David Monniaux <David.Monniaux@univ-grenoble-alpes.fr> | 2021-10-29 21:56:59 +0200 |
| commit | ae2d228c04f4fca1e281b146764646cbdd7d6b1d (patch) | |
| tree | 244f88aebc77a9ca2ef7e69731deb1dfee434ece /lib/Maps.v | |
| parent | e19d179d1f30d5893e5f30dbd33188350656831e (diff) | |
| parent | d194e47a7d494944385ff61c194693f8a67787cb (diff) | |
| download | compcert-kvx-ae2d228c04f4fca1e281b146764646cbdd7d6b1d.tar.gz compcert-kvx-ae2d228c04f4fca1e281b146764646cbdd7d6b1d.zip | |
Merge remote-tracking branch 'origin/master' into towards_3.10
Diffstat (limited to 'lib/Maps.v')
| -rw-r--r-- | lib/Maps.v | 4 |
1 files changed, 2 insertions, 2 deletions
@@ -1761,7 +1761,7 @@ Proof. intros. transitivity a0; auto. Qed. -Instance Equal_Equivalence : Equivalence Equal := { +Global Instance Equal_Equivalence : Equivalence Equal := { Equivalence_Reflexive := Equal_refl; Equivalence_Symmetric := Equal_sym; Equivalence_Transitive := Equal_trans @@ -1790,7 +1790,7 @@ Next Obligation. unfold equiv, complement in H0. congruence. Qed. -Instance Equal_EqDec : EqDec (T.t A) Equal := Equal_dec. +Global Instance Equal_EqDec : EqDec (T.t A) Equal := Equal_dec. End EXTENSIONAL_EQUALITY. |