From 17818cb05e56a1e86924b577abb706a41f629b15 Mon Sep 17 00:00:00 2001
From: Hai Dang <dhhai.uns@gmail.com>
Date: Tue, 21 Feb 2017 11:48:13 +0100
Subject: [PATCH] fix last commit

---
 coq/ra/base/ghosts.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/coq/ra/base/ghosts.v b/coq/ra/base/ghosts.v
index aed4269c..ca0d073d 100644
--- a/coq/ra/base/ghosts.v
+++ b/coq/ra/base/ghosts.v
@@ -366,7 +366,7 @@ Section Exclusives.
   Lemma gmapR_singleton_Exclusive (i: K) (x y: A) `{!Exclusive x}:
     ✓ ({[i := x]} ⋅ {[i := y]}) → False.
   Proof.
-    intros ?. rewrite op_singleton. move/(_ i). rewrite lookup_singleton.
+    rewrite op_singleton. move/(_ i). rewrite lookup_singleton.
     by apply exclusive_l.
   Qed.
 
-- 
GitLab