diff options
| author | Yann Herklotz <git@yannherklotz.com> | 2023-06-25 17:53:22 +0100 |
|---|---|---|
| committer | Yann Herklotz <git@yannherklotz.com> | 2023-06-25 17:53:22 +0100 |
| commit | e9f748f8e302f4d9977661e9c51ddaf5410bdec6 (patch) | |
| tree | 01c04d7e5770d4e927da40052f17eff48e7d8079 /src/hls/GiblePargenproofForward.v | |
| parent | 9134c30e5c9a46299aacc94dd5664308bd554303 (diff) | |
| download | vericert-e9f748f8e302f4d9977661e9c51ddaf5410bdec6.tar.gz vericert-e9f748f8e302f4d9977661e9c51ddaf5410bdec6.zip | |
Finish mutual exclusivity check
Diffstat (limited to 'src/hls/GiblePargenproofForward.v')
| -rw-r--r-- | src/hls/GiblePargenproofForward.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/src/hls/GiblePargenproofForward.v b/src/hls/GiblePargenproofForward.v index 3d0f7d5..946a243 100644 --- a/src/hls/GiblePargenproofForward.v +++ b/src/hls/GiblePargenproofForward.v @@ -421,7 +421,7 @@ all be evaluable. apply sem_pexpr_Pand. destruct b. constructor. right. eapply sem_update_Isetpred; eauto. - { unfold assert_ in Heqo. destr. auto using check_mutexcl_correct. } + { unfold assert_ in Heqo. destr. eauto using check_mutexcl_correct. } constructor. constructor. replace false with (negb true) by auto. apply sem_pexpr_negate. inv TRUTHY. constructor. cbn. eapply sem_pexpr_eval. inv PRED. eauto. auto. @@ -429,7 +429,7 @@ all be evaluable. apply sem_pexpr_negate. eapply sem_pexpr_eval. inv PRED. eauto. auto. eapply sem_update_Isetpred; eauto. - { unfold assert_ in Heqo. destr. auto using check_mutexcl_correct. } + { unfold assert_ in Heqo. destr. eauto using check_mutexcl_correct. } constructor. constructor. constructor. replace true with (negb false) by auto. apply sem_pexpr_negate. eapply sem_pexpr_eval. inv PRED. eauto. inv TRUTHY. auto. cbn -[eval_predf]. |