diff options
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. |