diff options
| author | Yann Herklotz <git@yannherklotz.com> | 2022-06-05 11:11:09 +0100 |
|---|---|---|
| committer | Yann Herklotz <git@yannherklotz.com> | 2022-06-05 11:11:09 +0100 |
| commit | 2e731050c69c98142d29d87fb863f199d50dfe19 (patch) | |
| tree | 20a2206cf8c902ee612d9f05bbd8e022dadd632e | |
| parent | 7e15dbdfc2a1708d36127f86302bdb3ae5bfae21 (diff) | |
| download | vericert-2e731050c69c98142d29d87fb863f199d50dfe19.tar.gz vericert-2e731050c69c98142d29d87fb863f199d50dfe19.zip | |
Remove inv H1 from condelim proof
| -rw-r--r-- | src/hls/CondElimproof.v | 6 |
1 files changed, 3 insertions, 3 deletions
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', |