From c6ebd73465ef895c6ea5e240f9c784463a6a0fe5 Mon Sep 17 00:00:00 2001
From: David Monniaux <david.monniaux@univ-grenoble-alpes.fr>
Date: Thu, 12 Mar 2020 16:46:06 +0100
Subject: removed second analysis phase

---
 backend/CSE3proof.v | 2 ++
 1 file changed, 2 insertions(+)

(limited to 'backend/CSE3proof.v')

diff --git a/backend/CSE3proof.v b/backend/CSE3proof.v
index c7a882b6..72b3e7e1 100644
--- a/backend/CSE3proof.v
+++ b/backend/CSE3proof.v
@@ -76,6 +76,8 @@ Proof.
   destruct f; simpl; intros.
   - monadInv H.
     monadInv EQ.
+    destruct preanalysis.
+    inv EQ1.
     reflexivity.
   - monadInv H.
     reflexivity.
-- 
cgit