aboutsummaryrefslogtreecommitdiffstats
path: root/backend/CSE3proof.v
diff options
context:
space:
mode:
authorDavid Monniaux <david.monniaux@univ-grenoble-alpes.fr>2020-03-12 16:46:06 +0100
committerDavid Monniaux <david.monniaux@univ-grenoble-alpes.fr>2020-03-12 16:46:06 +0100
commitc6ebd73465ef895c6ea5e240f9c784463a6a0fe5 (patch)
tree15dec58036a4ddf49954cd25565b50e17bc1b292 /backend/CSE3proof.v
parent9efb4d87c549087e2ef16103a6993a1f99328348 (diff)
downloadcompcert-kvx-c6ebd73465ef895c6ea5e240f9c784463a6a0fe5.tar.gz
compcert-kvx-c6ebd73465ef895c6ea5e240f9c784463a6a0fe5.zip
removed second analysis phase
Diffstat (limited to 'backend/CSE3proof.v')
-rw-r--r--backend/CSE3proof.v2
1 files changed, 2 insertions, 0 deletions
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.