From 5599f3d12779d9dbac3314bca32c19054912df53 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Mon, 28 Aug 2017 10:53:10 +0200
Subject: [PATCH] Change the order of some IntoWand premises to avoid
 backtracking.

Otherwise, whenever it cannot establish the Absorbing or Affine premise,
it will backtrack on the FromAssumption premise, causing a possible loop.
No idea why this happens, this may be a Coq bug...
---
 theories/proofmode/class_instances.v | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

diff --git a/theories/proofmode/class_instances.v b/theories/proofmode/class_instances.v
index c7409798a..25413547e 100644
--- a/theories/proofmode/class_instances.v
+++ b/theories/proofmode/class_instances.v
@@ -164,19 +164,19 @@ Proof.
 Qed.
 
 Global Instance into_wand_impl_false_true P Q P' :
-  FromAssumption true P P' → Absorbing P' →
+  Absorbing P' → FromAssumption true P P' →
   IntoWand false true (P' → Q) P Q.
 Proof.
-  rewrite /IntoWand /FromAssumption /= => HP ?. apply wand_intro_l.
+  rewrite /IntoWand /FromAssumption /= => ? HP. apply wand_intro_l.
   rewrite -(bare_persistently_idemp P) HP.
   by rewrite -persistently_and_bare_sep_l persistently_elim_absorbing impl_elim_r.
 Qed.
 
 Global Instance into_wand_impl_true_false P Q P' :
-  FromAssumption false P P' → Affine P' →
+  Affine P' → FromAssumption false P P' →
   IntoWand true false (P' → Q) P Q.
 Proof.
-  rewrite /FromAssumption /IntoWand /= => HP ?. apply wand_intro_r.
+  rewrite /FromAssumption /IntoWand /= => ? HP. apply wand_intro_r.
   rewrite -persistently_and_bare_sep_l HP -{2}(affine_bare P') bare_and_l -bare_and_r.
   by rewrite bare_persistently_elim impl_elim_l.
 Qed.
-- 
GitLab