From 70afd76edfdbdf121678e04b23ff18d097013428 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Mon, 6 Jun 2016 11:08:08 -0400
Subject: [PATCH] Turn some "case _ :" occurences into "case:'.

---
 algebra/gmap.v | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/algebra/gmap.v b/algebra/gmap.v
index bbb295498..bf6d49a34 100644
--- a/algebra/gmap.v
+++ b/algebra/gmap.v
@@ -314,12 +314,12 @@ Proof.
   intros ?? Hx HQ. apply cmra_total_updateP=> n gf Hg.
   destruct (Hx n (gf !! i)) as (y&?&Hy).
   { move:(Hg i). rewrite !left_id.
-    case _: (gf !! i)=>[x|]; rewrite /= ?left_id //.
+    case: (gf !! i)=>[x|]; rewrite /= ?left_id //.
     intros; by apply cmra_valid_validN. }
   exists {[ i := y ]}; split; first by auto.
   intros i'; destruct (decide (i' = i)) as [->|].
   - rewrite lookup_op lookup_singleton.
-    move:Hy; case _: (gf !! i)=>[x|]; rewrite /= ?right_id //.
+    move:Hy; case: (gf !! i)=>[x|]; rewrite /= ?right_id //.
   - move:(Hg i'). by rewrite !lookup_op lookup_singleton_ne // !left_id.
 Qed.
 Lemma singleton_updateP_unit' (P: A → Prop) u i :
-- 
GitLab