From c19ecc9326d0278989d7651bf8c8cf0d1c387235 Mon Sep 17 00:00:00 2001 From: Léo Gourdin Date: Sat, 6 Mar 2021 12:36:11 +0100 Subject: Adding a mini CSE pass in the expansion oracle --- scheduling/RTLpathSE_impl.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'scheduling/RTLpathSE_impl.v') 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. -- cgit