diff options
| author | Sylvain Boulmé <sylvain.boulme@univ-grenoble-alpes.fr> | 2020-10-12 16:27:24 +0200 |
|---|---|---|
| committer | Sylvain Boulmé <sylvain.boulme@univ-grenoble-alpes.fr> | 2020-10-12 16:27:24 +0200 |
| commit | 3a56ef38c7ec2c930312e7f574c66d4e3fd79983 (patch) | |
| tree | 3f5c8cb3fc19e77252fcdd291b43a11c07cb296e /kvx | |
| parent | 4407e230c5408161b287068cf60f670c162ecf5b (diff) | |
| download | compcert-kvx-3a56ef38c7ec2c930312e7f574c66d4e3fd79983.tar.gz compcert-kvx-3a56ef38c7ec2c930312e7f574c66d4e3fd79983.zip | |
simpl hsstate_simu_core_correct
Diffstat (limited to 'kvx')
| -rw-r--r-- | kvx/lib/RTLpathSE_impl_junk.v | 4 |
1 files changed, 1 insertions, 3 deletions
diff --git a/kvx/lib/RTLpathSE_impl_junk.v b/kvx/lib/RTLpathSE_impl_junk.v index af430918..4fb69d18 100644 --- a/kvx/lib/RTLpathSE_impl_junk.v +++ b/kvx/lib/RTLpathSE_impl_junk.v @@ -1898,9 +1898,7 @@ Theorem hsstate_simu_core_correct dm f ctx hst1 hst2: hsstate_simu_core dm f hst1 hst2 -> hsstate_simu dm f hst1 hst2 ctx. Proof. - intros (SCORE & FSIMU). intros st1 st2 HREF1 HREF2. - destruct HREF1 as (SREF1 & DREF1 & FREF1). destruct HREF2 as (SREF2 & DREF2 & FREF2). - assert (PCEQ: dm ! (hsi_pc hst2) = Some (hsi_pc hst1)) by apply SCORE. + intros (SCORE & FSIMU) st1 st2 (SREF1 & DREF1 & FREF1) (SREF2 & DREF2 & FREF2). generalize SCORE. intro SIMU; eapply hsistate_simu_core_correct in SIMU; eauto. constructor; auto. intros is1 SEM1 CONT1. |