1 files changed, 4 insertions, 2 deletions
diff --git a/x86/Asm.v b/x86/Asm.v
index 799b533e..b9c4817a 100644
--- a/x86/Asm.v
+++ b/x86/Asm.v
@@ -877,6 +877,10 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out
       Next (nextinstr (compare_floats (rs r1) (rs r2) rs)) m
   | Pxorpd_f rd =>
       Next (nextinstr_nf (rs#rd <- (Vfloat Float.zero))) m
+  | Pmaxsd rd r1 =>
+      Next (nextinstr (rs#rd <- (Op.maxf rs#rd rs#r1))) m
+  | Pminsd rd r1 =>
+      Next (nextinstr (rs#rd <- (Op.minf rs#rd rs#r1))) m
   (** Arithmetic operations over single-precision floats *)
   | Padds_ff rd r1 =>
       Next (nextinstr (rs#rd <- (Val.addfs rs#rd rs#r1))) m
@@ -996,8 +1000,6 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out
   | Pfnmsub132 _ _ _
   | Pfnmsub213 _ _ _
   | Pfnmsub231 _ _ _
-  | Pmaxsd _ _
-  | Pminsd _ _
   | Pmovb_rm _ _
   | Pmovq_rf _ _
   | Pmovsq_rm _ _