From a8dd20cd96a1c8636add5b8b45b6ee5ff5982f9a Mon Sep 17 00:00:00 2001
From: David Monniaux <david.monniaux@univ-grenoble-alpes.fr>
Date: Thu, 9 Jan 2020 17:43:52 +0100
Subject: fix move

---
 backend/ForwardMovesproof.v | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

(limited to 'backend/ForwardMovesproof.v')

diff --git a/backend/ForwardMovesproof.v b/backend/ForwardMovesproof.v
index 8e2ba9af..b1425401 100644
--- a/backend/ForwardMovesproof.v
+++ b/backend/ForwardMovesproof.v
@@ -470,8 +470,10 @@ Proof.
     simpl in H0.
     destruct (map # pc') as [mpc' | ] in *; try discriminate.
     simpl in GE.
-    unfold move in GE.
+    admit.
+    admit.
   }
+  admit.
   
 (* load *)
 - econstructor; split.
-- 
cgit