From ded5a15a0ebcda4d11af32b3c4a46048b11e3c91 Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Thu, 30 Jun 2022 23:40:43 +0100 Subject: Remove useless comments --- src/hls/IfConversionproof.v | 9 --------- 1 file changed, 9 deletions(-) (limited to 'src') diff --git a/src/hls/IfConversionproof.v b/src/hls/IfConversionproof.v index 0b01e83..39ec046 100644 --- a/src/hls/IfConversionproof.v +++ b/src/hls/IfConversionproof.v @@ -53,9 +53,6 @@ Variant match_stackframe : stackframe -> stackframe -> Prop := (TF: transf_function f = tf), match_stackframe (Stackframe res f sp pc rs p) (Stackframe res tf sp pc rs p). -(* c ! pc = fc ! pc *) -(* \/ (c ! pc = a ++ fc ! pc' ++ b /\ fc ! pc = a ++ if p goto pc' ++ b) *) - Definition bool_order (b: bool): nat := if b then 1 else 0. Inductive if_conv_block_spec (c: code): SeqBB.t -> SeqBB.t -> Prop := @@ -300,12 +297,6 @@ Section CORRECTNESS. f.(fn_code) ! pc = Some block2 -> SeqBB.step tge sp in_s' block2 out_s. - (* (EXT: sem_extrap tf pc0 sp (Iexec (mki rs p m)) (Iexec (mki rs0 p0 m0)) b) - (STAR: star step ge (State stk f sp pc0 rs0 p0 m0) E0 (State stk f sp pc rs p m)) - (IS_B: exists b, f.(fn_code)!pc0 = Some b) - (SPEC: forall b_o, f.(fn_code) ! pc = Some b_o -> if_conv_block_spec f.(fn_code) b_o b), - *) - Variant match_states : option SeqBB.t -> state -> state -> Prop := | match_state_some : forall stk stk' f tf sp pc rs p m b pc0 rs0 p0 m0 -- cgit