diff options
Diffstat (limited to 'mppa_k1c/Asm.v')
| -rw-r--r-- | mppa_k1c/Asm.v | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/mppa_k1c/Asm.v b/mppa_k1c/Asm.v index bb78eda1..b5051de3 100644 --- a/mppa_k1c/Asm.v +++ b/mppa_k1c/Asm.v @@ -88,6 +88,9 @@ Inductive instruction : Type := | Pdinval
| Pdinvall (addr: ireg)
| Pdtouchl (addr: ireg)
+ | Piinval
+ | Piinvals (addr: ireg)
+ | Pitouchl (addr: ireg)
| Pdzerol (addr: ireg)
(** Loads **)
|