From 38df0d21f743af2f97345049621e9ddd7f6fbb31 Mon Sep 17 00:00:00 2001
From: "Paolo G. Giarrusso" <p.giarrusso@gmail.com>
Date: Tue, 7 Jan 2020 06:03:44 +0100
Subject: [PATCH] Rename Awesome_{ne,proper} to NamespaceMap_{ne,proper}

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

diff --git a/theories/algebra/namespace_map.v b/theories/algebra/namespace_map.v
index 72949d1b2..db80ca2ac 100644
--- a/theories/algebra/namespace_map.v
+++ b/theories/algebra/namespace_map.v
@@ -46,9 +46,9 @@ Instance namespace_map_dist : Dist (namespace_map A) := λ n x y,
   namespace_map_data_proj x ≡{n}≡ namespace_map_data_proj y ∧
   namespace_map_token_proj x = namespace_map_token_proj y.
 
-Global Instance Awesome_ne : NonExpansive2 (@NamespaceMap A).
+Global Instance NamespaceMap_ne : NonExpansive2 (@NamespaceMap A).
 Proof. by split. Qed.
-Global Instance Awesome_proper : Proper ((≡) ==> (=) ==> (≡)) (@NamespaceMap A).
+Global Instance NamespaceMap_proper : Proper ((≡) ==> (=) ==> (≡)) (@NamespaceMap A).
 Proof. by split. Qed.
 Global Instance namespace_map_data_proj_ne: NonExpansive (@namespace_map_data_proj A).
 Proof. by destruct 1. Qed.
-- 
GitLab