From 7bb734bc4328cee6b6a2ad6d45821a0ec15ab01c Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Wed, 20 Jan 2021 13:02:38 +0100
Subject: [PATCH] =?UTF-8?q?Rename=20instance=20`finmap=5Flookup=5Ftotal`?=
 =?UTF-8?q?=20=E2=86=92=20`map=5Flookup=5Ftotal`.?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 theories/fin_maps.v | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/theories/fin_maps.v b/theories/fin_maps.v
index d23895b0..724d2534 100644
--- a/theories/fin_maps.v
+++ b/theories/fin_maps.v
@@ -145,9 +145,9 @@ Fixpoint map_seq `{Insert nat A M, Empty M} (start : nat) (xs : list A) : M :=
   | x :: xs => <[start:=x]> (map_seq (S start) xs)
   end.
 
-Global Instance finmap_lookup_total `{!Lookup K A (M A), !Inhabited A} :
+Global Instance map_lookup_total `{!Lookup K A (M A), !Inhabited A} :
   LookupTotal K A (M A) | 20 := λ i m, default inhabitant (m !! i).
-Typeclasses Opaque finmap_lookup_total.
+Typeclasses Opaque map_lookup_total.
 
 (** * Theorems *)
 Section theorems.
@@ -174,7 +174,7 @@ Section setoid.
     Proper (≡@{A}) inhabitant →
     Proper ((≡@{M A}) ==> (≡)) (lookup_total i).
   Proof.
-    intros ? m1 m2 Hm. unfold lookup_total, finmap_lookup_total.
+    intros ? m1 m2 Hm. unfold lookup_total, map_lookup_total.
     apply from_option_proper; auto. by intros ??.
   Qed.
   Global Instance partial_alter_proper :
-- 
GitLab