From 144d62b0bc3b86c60bdb73aa56a76a680bb66742 Mon Sep 17 00:00:00 2001
From: Tej Chajed <tchajed@mit.edu>
Date: Sat, 15 Feb 2020 19:47:47 +0100
Subject: [PATCH] Remove useless implicit annotation on binder

Fixes a new warning on Coq 8.12+alpha when implicit annotations are used
in positions where they are ignored.
---
 theories/proofmode/environments.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/theories/proofmode/environments.v b/theories/proofmode/environments.v
index 78a8d28ca..4af44c52a 100644
--- a/theories/proofmode/environments.v
+++ b/theories/proofmode/environments.v
@@ -263,7 +263,7 @@ Proof. by eexists. Qed.
 Definition envs_entails {PROP : bi} (Δ : envs PROP) (Q : PROP) : Prop :=
   envs_entails_aux.(unseal) PROP (env_intuitionistic Δ) (env_spatial Δ) Q.
 Definition envs_entails_eq :
-  @envs_entails = λ {PROP} (Δ : envs PROP) Q, (of_envs Δ ⊢ Q).
+  @envs_entails = λ PROP (Δ : envs PROP) Q, (of_envs Δ ⊢ Q).
 Proof. by rewrite /envs_entails envs_entails_aux.(seal_eq). Qed.
 Arguments envs_entails {PROP} Δ Q%I : rename.
 Instance: Params (@envs_entails) 1 := {}.
-- 
GitLab