diff options
| author | Léo Gourdin <leo.gourdin@univ-grenoble-alpes.fr> | 2021-03-06 12:36:11 +0100 |
|---|---|---|
| committer | Léo Gourdin <leo.gourdin@univ-grenoble-alpes.fr> | 2021-03-06 12:36:11 +0100 |
| commit | c19ecc9326d0278989d7651bf8c8cf0d1c387235 (patch) | |
| tree | 479bd06ca0ed2e2d14900a78c93914537e4a7d91 /scheduling/RTLpathSE_impl.v | |
| parent | 3e953ef41f736ed5b7db699b1adf21d46cb5b8db (diff) | |
| download | compcert-kvx-c19ecc9326d0278989d7651bf8c8cf0d1c387235.tar.gz compcert-kvx-c19ecc9326d0278989d7651bf8c8cf0d1c387235.zip | |
Adding a mini CSE pass in the expansion oracle
Diffstat (limited to 'scheduling/RTLpathSE_impl.v')
| -rw-r--r-- | scheduling/RTLpathSE_impl.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/scheduling/RTLpathSE_impl.v b/scheduling/RTLpathSE_impl.v index 12aba56b..e21d7cd1 100644 --- a/scheduling/RTLpathSE_impl.v +++ b/scheduling/RTLpathSE_impl.v @@ -819,7 +819,7 @@ Proof. rewrite <- X, sok_local_set_sreg. intuition eauto. - destruct REF; intuition eauto. - generalize REF; intros (OKEQ & _). rewrite OKEQ in * |-; erewrite red_PTree_set_refines; eauto. - Qed. +Qed. Global Opaque hslocal_set_sreg. Local Hint Resolve hslocal_set_sreg_correct: wlp. |