diff options
Diffstat (limited to 'x86/Asm.v')
-rw-r--r-- | x86/Asm.v | 2 |
1 files changed, 0 insertions, 2 deletions
@@ -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 _ _ |