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