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 /x86 | |
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 'x86')
-rw-r--r-- | x86/Machregs.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/x86/Machregs.v b/x86/Machregs.v index 6f3064b8..a440bffc 100644 --- a/x86/Machregs.v +++ b/x86/Machregs.v @@ -57,9 +57,9 @@ Proof. intros. specialize (H r). InvBooleans. auto. Qed. -Instance Decidable_eq_mreg : forall (x y: mreg), Decidable (eq x y) := Decidable_eq mreg_eq. +Global Instance Decidable_eq_mreg : forall (x y: mreg), Decidable (eq x y) := Decidable_eq mreg_eq. -Instance Finite_mreg : Finite mreg := { +Global Instance Finite_mreg : Finite mreg := { Finite_elements := all_mregs; Finite_elements_spec := all_mregs_complete }. |