From 1f38df638dfd4ae2aa85467cc28f6b4fa1da03b1 Mon Sep 17 00:00:00 2001
From: Cyril SIX <cyril.six@kalray.eu>
Date: Tue, 12 Feb 2019 11:57:16 +0100
Subject: Minor refactorization

---
 mppa_k1c/PostpassScheduling.v      | 12 ++++++++++++
 mppa_k1c/PostpassSchedulingproof.v | 12 ------------
 2 files changed, 12 insertions(+), 12 deletions(-)

diff --git a/mppa_k1c/PostpassScheduling.v b/mppa_k1c/PostpassScheduling.v
index ef455e39..10331f15 100644
--- a/mppa_k1c/PostpassScheduling.v
+++ b/mppa_k1c/PostpassScheduling.v
@@ -71,6 +71,18 @@ Next Obligation.
     apply (H ef args res). contradict H1. auto.
 Qed.
 
+Lemma concat2_zlt_size:
+  forall a b bb,
+  concat2 a b = OK bb ->
+     size a <= Ptrofs.max_unsigned
+  /\ size b <= Ptrofs.max_unsigned.
+Proof.
+  intros. monadInv H.
+  split.
+  - unfold check_size in EQ. destruct (zlt Ptrofs.max_unsigned (size a)); monadInv EQ. omega.
+  - unfold check_size in EQ1. destruct (zlt Ptrofs.max_unsigned (size b)); monadInv EQ1. omega.
+Qed.
+
 Lemma concat2_noexit:
   forall a b bb,
   concat2 a b = OK bb ->
diff --git a/mppa_k1c/PostpassSchedulingproof.v b/mppa_k1c/PostpassSchedulingproof.v
index 19d30354..d0aa89a4 100644
--- a/mppa_k1c/PostpassSchedulingproof.v
+++ b/mppa_k1c/PostpassSchedulingproof.v
@@ -36,18 +36,6 @@ Inductive bblock_equiv (ge: Genv.t fundef unit) (f: function) (bb bb': bblock) :
       exec_bblock ge f bb rs m = exec_bblock ge f bb' rs m) ->
       bblock_equiv ge f bb bb'.
 
-Lemma concat2_zlt_size:
-  forall a b bb,
-  concat2 a b = OK bb ->
-     size a <= Ptrofs.max_unsigned
-  /\ size b <= Ptrofs.max_unsigned.
-Proof.
-  intros. monadInv H.
-  split.
-  - unfold check_size in EQ. destruct (zlt Ptrofs.max_unsigned (size a)); monadInv EQ. omega.
-  - unfold check_size in EQ1. destruct (zlt Ptrofs.max_unsigned (size b)); monadInv EQ1. omega.
-Qed.
-
 (* Axioms that verified_schedule must verify *)
 Axiom verified_schedule_correct:
   forall ge f bb lbb,
-- 
cgit