From dba20d6c8201c1271ebda9f228ad95c77c6ca8a6 Mon Sep 17 00:00:00 2001
From: Yann Herklotz <git@yannherklotz.com>
Date: Tue, 5 Apr 2022 14:37:11 +0100
Subject: Add basic blocks to the stackframe

---
 src/hls/RTLPargenproof.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'src/hls/RTLPargenproof.v')

diff --git a/src/hls/RTLPargenproof.v b/src/hls/RTLPargenproof.v
index 215aef5..fac6455 100644
--- a/src/hls/RTLPargenproof.v
+++ b/src/hls/RTLPargenproof.v
@@ -631,7 +631,7 @@ Qed.
 
 Lemma step_instr_seq_matches :
   forall a ge sp st st',
-  step_instr_seq ge sp st a st' ->
+   step_instr_seq ge sp st a st' ->
   forall tst, match_states st tst ->
               exists tst', step_instr_seq ge sp tst a tst'
                            /\ match_states st' tst'.
-- 
cgit