From 11dc19dc169d99a944abb4144ea67eb4fc03f883 Mon Sep 17 00:00:00 2001
From: David Monniaux <david.monniaux@univ-grenoble-alpes.fr>
Date: Tue, 10 Mar 2020 15:06:12 +0100
Subject: moved no away

---
 backend/CSE3analysisproof.v | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

(limited to 'backend/CSE3analysisproof.v')

diff --git a/backend/CSE3analysisproof.v b/backend/CSE3analysisproof.v
index e2ce6b5d..a1e57eb5 100644
--- a/backend/CSE3analysisproof.v
+++ b/backend/CSE3analysisproof.v
@@ -485,10 +485,10 @@ Section SOUNDNESS.
     sem_rel rel rs m ->
     sem_rhs sop args rs m  v ->
     ~ In dst args ->
-    eq_find (ctx := ctx)
-            no {| eq_lhs := dst;
-                  eq_op  := sop;
-                  eq_args:= args |} = Some eqno ->
+    eq_find (ctx := ctx) no
+            {| eq_lhs := dst;
+               eq_op  := sop;
+               eq_args:= args |} = Some eqno ->
     sem_rel (PSet.add eqno (kill_reg (ctx := ctx) dst rel)) (rs # dst <- v) m.
   Proof.
     intros until v.
-- 
cgit