1 files changed, 0 insertions, 2 deletions
diff --git a/x86/Asm.v b/x86/Asm.v
index 58e28c40..bbed28cb 100644
--- a/x86/Asm.v
+++ b/x86/Asm.v
@@ -284,7 +284,6 @@ Inductive instruction: Type :=
   | Pmovsb
   | Pmovsw
   | Pmovw_rm (rd: ireg) (ad: addrmode)
-  | Pnop
   | Prep_movsl
   | Psbbl_rr (rd: ireg) (r2: ireg)
   | Psqrtsd (rd: freg) (r1: freg)
@@ -1003,7 +1002,6 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out
   | Pmovsb
   | Pmovsw
   | Pmovw_rm _ _
-  | Pnop
   | Prep_movsl
   | Psbbl_rr _ _
   | Psqrtsd _ _