From de8e08df45d42fb5dc5ec6f98d921c507777243d Mon Sep 17 00:00:00 2001
From: "Paolo G. Giarrusso" <p.giarrusso@gmail.com>
Date: Thu, 7 Nov 2019 20:57:39 +0100
Subject: [PATCH] Fix ssreflect warning on Coq 8.10

Since Coq 8.10, `move => {}e` means `move => {e}e`.
For the backward-compatible syntax and discussion, see
https://github.com/coq/coq/issues/10550#issuecomment-542397265.
---
 theories/bi/tactics.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/theories/bi/tactics.v b/theories/bi/tactics.v
index 983a5d8d4..feb33d0fb 100644
--- a/theories/bi/tactics.v
+++ b/theories/bi/tactics.v
@@ -81,7 +81,7 @@ Module bi_reflection. Section bi_reflection.
   Lemma flatten_cancel e e' ns :
     cancel ns e = Some e' → flatten e ≡ₚ ns ++ flatten e'.
   Proof.
-    rewrite /cancel fmap_Some=> -[{e'}e' [He ->]]; rewrite flatten_prune.
+    rewrite /cancel fmap_Some=> -[{e'}-e' [He ->]]; rewrite flatten_prune.
     revert e' He; induction ns as [|n ns IH]=> e' He; simplify_option_eq; auto.
     rewrite Permutation_middle -flatten_cancel_go //; eauto.
   Qed.
-- 
GitLab