From 2e731050c69c98142d29d87fb863f199d50dfe19 Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Sun, 5 Jun 2022 11:11:09 +0100 Subject: Remove inv H1 from condelim proof --- src/hls/CondElimproof.v | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) (limited to 'src/hls/CondElimproof.v') diff --git a/src/hls/CondElimproof.v b/src/hls/CondElimproof.v index ace90b0..ecc3538 100644 --- a/src/hls/CondElimproof.v +++ b/src/hls/CondElimproof.v @@ -409,13 +409,13 @@ Section CORRECTNESS. Proof. inversion 1; subst; simplify; clear H; match goal with H: context[match_states] |- _ => inv H end. - - inv H1. do 2 econstructor. rewrite <- sig_transf_function. econstructor; eauto. + - do 2 econstructor. rewrite <- sig_transf_function. econstructor; eauto. eauto using find_function_translated. auto. econstructor; auto. repeat (constructor; auto). - - inv H1. do 2 econstructor. econstructor. eauto using find_function_translated. + - do 2 econstructor. econstructor. eauto using find_function_translated. eauto using sig_transf_function. eauto. econstructor; auto. - - inv H2. + - do 2 econstructor. Lemma step_list2_ge : forall sp l i i', -- cgit