From 246553dadbf6a089bd92bcdea645cff95e26f3ed Mon Sep 17 00:00:00 2001
From: Léo Gourdin <leo.gourdin@univ-grenoble-alpes.fr>
Date: Sun, 6 Dec 2020 22:15:54 +0100
Subject: Asmgen proof completely proved with ldp/stp

---
 aarch64/Asmblockdeps.v | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

(limited to 'aarch64/Asmblockdeps.v')

diff --git a/aarch64/Asmblockdeps.v b/aarch64/Asmblockdeps.v
index bdfb9ed3..e2d788a5 100644
--- a/aarch64/Asmblockdeps.v
+++ b/aarch64/Asmblockdeps.v
@@ -1781,8 +1781,9 @@ Local Ltac preg_eq_discr r rd :=
       * rewrite e; rewrite Pregmap.gss, sr_gss; auto.
       * rewrite Pregmap.gso, !assign_diff; auto; apply ppos_discr in n; auto.
     + rewrite <- sp_xsp; rewrite MLOAD; reflexivity.
-(*Qed.*)
-Admitted.
+  - (* Nop *)
+    Simpl sr.
+Qed.
 
 Theorem bisimu_body:
   forall bdy rsr mr sr,
-- 
cgit