From 4dda9d08fb91bad239a22629bf2dd782c581b5e0 Mon Sep 17 00:00:00 2001
From: Jacques-Henri Jourdan <jacques-henri.jourdan@normalesup.org>
Date: Thu, 15 Sep 2016 23:40:29 +0200
Subject: [PATCH] Change hypotheses order for [frame_later] for better perfs.

---
 proofmode/class_instances.v | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/proofmode/class_instances.v b/proofmode/class_instances.v
index 3e0504e93..aba0e60c1 100644
--- 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.
-- 
GitLab