1 files changed, 2 insertions, 0 deletions
diff --git a/mppa_k1c/Asm.v b/mppa_k1c/Asm.v
index b5051de3..a9a88d75 100644
--- a/mppa_k1c/Asm.v
+++ b/mppa_k1c/Asm.v
@@ -92,6 +92,8 @@ Inductive instruction : Type :=
   | Piinvals (addr: ireg)
   | Pitouchl (addr: ireg)
   | Pdzerol (addr: ireg)
+  | Pafaddd (addr: ireg) (incr_res: ireg)
+  | Pafaddw (addr: ireg) (incr_res: ireg)
             
   (** Loads **)
   | Plb     (rd: ireg) (ra: ireg) (ofs: addressing)     (**r load byte *)