From ece46e22da61e8a8d40766c533bcf2dd760deccb Mon Sep 17 00:00:00 2001
From: Yann Herklotz <git@yannherklotz.com>
Date: Sat, 23 Jan 2021 11:54:11 +0000
Subject: Remove match on basic blocks

---
 src/hls/RTLPargenproof.v | 6 ------
 1 file changed, 6 deletions(-)

(limited to 'src')

diff --git a/src/hls/RTLPargenproof.v b/src/hls/RTLPargenproof.v
index 05001ce..14220d3 100644
--- a/src/hls/RTLPargenproof.v
+++ b/src/hls/RTLPargenproof.v
@@ -41,12 +41,6 @@ Inductive match_states: RTLBlock.state -> RTLPar.state -> Prop :=
       (STACKS: list_forall2 match_stackframes sf sf'),
       match_states (RTLBlock.State sf f sp pc rs mem)
                    (RTLPar.State sf' tf sp pc rs mem)
-| match_block:
-    forall sf sf' f tf sp cfi rs mem
-      (TRANSL: transl_function f = OK tf)
-      (STACKS: list_forall2 match_stackframes sf sf'),
-      match_states (RTLBlock.Block sf f sp cfi rs mem)
-                   (RTLPar.Block sf' tf sp (mk_bblock nil cfi) rs mem)
 | match_returnstate:
     forall stack stack' v mem
       (STACKS: list_forall2 match_stackframes stack stack'),
-- 
cgit