From 4d79ef052cc05240d6613bb22ef1ec547b17d3e1 Mon Sep 17 00:00:00 2001
From: David Monniaux <david.monniaux@univ-grenoble-alpes.fr>
Date: Thu, 29 Oct 2020 15:54:41 +0100
Subject: in CSE3 choose lowest variable as representative for moves

---
 backend/CSE3proof.v | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

(limited to 'backend/CSE3proof.v')

diff --git a/backend/CSE3proof.v b/backend/CSE3proof.v
index 3fbc9912..5dd5ee04 100644
--- a/backend/CSE3proof.v
+++ b/backend/CSE3proof.v
@@ -63,7 +63,7 @@ Proof.
     destruct rel as [rel | ]; simpl; intros.
     2: contradiction.
     eapply forward_move_sound; eauto.
-  Qed.
+Qed.
 
   Lemma forward_move_l_b_sound :
     forall rel rs m x,
@@ -447,7 +447,6 @@ Lemma step_simulation:
   forall S1 t S2, RTL.step ge S1 t S2 -> 
   forall S1', match_states S1 S1' ->
               exists S2', RTL.step tge S1' t S2' /\ match_states S2 S2'.
-Proof.
   induction 1; intros S1' MS; inv MS.
   - (* Inop *)
     exists (State ts tf sp pc' rs m). split.
-- 
cgit