Change hypotheses order for [frame_later] for better perfs.

4dda9d08 · Jacques-Henri Jourdan · e5c51505 · 4dda9d08
Commit 4dda9d08 authored Sep 15, 2016 by Jacques-Henri Jourdan
--- a/proofmode/class_instances.v
+++ b/proofmode/class_instances.v
@@ -270,9 +270,9 @@ Global Instance make_later_default P : MakeLater P (▷ P) | 100.
 Proof. done. Qed.

 Global Instance frame_later R R' P Q Q' :
-  Frame R P Q → MakeLater Q Q' → IntoLater R' R → Frame R' (▷ P) Q'.
+  IntoLater R' R → Frame R P Q → MakeLater Q Q' → Frame R' (▷ P) Q'.
 Proof.
-  rewrite /Frame /MakeLater /IntoLater=><- <- ->. by rewrite later_sep.
+  rewrite /Frame /MakeLater /IntoLater=>-> <- <-. by rewrite later_sep.
 Qed.

 Class MakeExceptLast (P Q : uPred M) := make_except_last : ◇ P ⊣⊢ Q.