From 5e3416d33ed2c72a13946afe4fd4ca9a5fecdd29 Mon Sep 17 00:00:00 2001 From: Robbert Krebbers <mail@robbertkrebbers.nl> Date: Thu, 8 Feb 2018 14:38:48 +0100 Subject: [PATCH] =?UTF-8?q?Fix=20issue=20#153=20by=20using=20`NoBackTrack`?= =?UTF-8?q?=20in=20the=20`Frame`=20instances=20for=20=E2=96=B7.?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- theories/proofmode/class_instances.v | 10 ++++++---- 1 file changed, 6 insertions(+), 4 deletions(-) diff --git a/theories/proofmode/class_instances.v b/theories/proofmode/class_instances.v index 61013accb..d3fdf8944 100644 --- a/theories/proofmode/class_instances.v +++ b/theories/proofmode/class_instances.v @@ -609,9 +609,10 @@ Global Instance make_later_default P : MakeLater P (▷ P) | 100. Proof. done. Qed. Global Instance frame_later p R R' P Q Q' : - IntoLaterN 1 R' R → Frame p R P Q → MakeLater Q Q' → Frame p R' (▷ P) Q'. + NoBackTrack (IntoLaterN 1 R' R) → + Frame p R P Q → MakeLater Q Q' → Frame p R' (▷ P) Q'. Proof. - rewrite /Frame /MakeLater /IntoLaterN=>-> <- <-. + rewrite /Frame /MakeLater /IntoLaterN=>-[->] <- <-. by rewrite persistently_if_later later_sep. Qed. @@ -622,9 +623,10 @@ Global Instance make_laterN_default P : MakeLaterN n P (▷^n P) | 100. Proof. done. Qed. Global Instance frame_laterN p n R R' P Q Q' : - IntoLaterN n R' R → Frame p R P Q → MakeLaterN n Q Q' → Frame p R' (▷^n P) Q'. + NoBackTrack (IntoLaterN n R' R) → + Frame p R P Q → MakeLaterN n Q Q' → Frame p R' (▷^n P) Q'. Proof. - rewrite /Frame /MakeLater /IntoLaterN=>-> <- <-. + rewrite /Frame /MakeLater /IntoLaterN=>-[->] <- <-. by rewrite persistently_if_laterN laterN_sep. Qed. -- GitLab