1 files changed, 4 insertions, 4 deletions
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.