From 05c77498f8f6b6f47a4669e0da79ec6f685e6722 Mon Sep 17 00:00:00 2001
From: Léo Gourdin <leo.gourdin@univ-grenoble-alpes.fr>
Date: Wed, 20 Jan 2021 19:31:49 +0100
Subject: Adding fp stores pair

---
 aarch64/Asmblock.v | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

(limited to 'aarch64/Asmblock.v')

diff --git a/aarch64/Asmblock.v b/aarch64/Asmblock.v
index f5d2abbe..c606002a 100644
--- a/aarch64/Asmblock.v
+++ b/aarch64/Asmblock.v
@@ -136,7 +136,8 @@ Inductive store_rs_a : Type :=
 Inductive store_rs1_rs2_a : Type :=
   | Pstpw
   | Pstpx
-  (* TODO *)
+  | Pstps
+  | Pstpd
   .
 
 Inductive st_instruction : Type :=
-- 
cgit