diff options
| -rw-r--r-- | src/hls/RTLPargenproof.v | 5 |
1 files changed, 4 insertions, 1 deletions
diff --git a/src/hls/RTLPargenproof.v b/src/hls/RTLPargenproof.v index 730ac98..0ff2312 100644 --- a/src/hls/RTLPargenproof.v +++ b/src/hls/RTLPargenproof.v @@ -171,4 +171,7 @@ Section CORRECTNESS. { destruct bb'; simplify; subst; repeat econstructor; eauto. } { destruct bb'; simplify; subst; repeat econstructor; eauto. } { destruct bb'; simplify; subst; repeat econstructor; eauto. } - { repeat econstructor; eauto. } + { unfold bind in *. destruct_match; try discriminate. repeat t. inv TRANSL0. + repeat econstructor; eauto. } + { inv TRANSL0. repeat econstructor; eauto using Events.external_call_symbols_preserved, symbols_preserved, senv_preserved, Events.E0_right. } + { inv STACKS. inv H1. repeat econstructor; eauto. } |