From 9271f6e39cc829e493978e3578fe082b75691bee Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Thu, 7 Nov 2019 15:34:04 +0100
Subject: [PATCH] More consistent name of projection for `AsEmpValid0` class.

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

diff --git a/theories/proofmode/classes.v b/theories/proofmode/classes.v
index e8eeb5d9d..2b678ed3c 100644
--- a/theories/proofmode/classes.v
+++ b/theories/proofmode/classes.v
@@ -498,9 +498,9 @@ Class AsEmpValid {PROP : bi} (φ : Prop) (P : PROP) :=
   as_emp_valid : φ ↔ bi_emp_valid P.
 Arguments AsEmpValid {_} _%type _%I.
 Class AsEmpValid0 {PROP : bi} (φ : Prop) (P : PROP) :=
-  as_emp_valid_here : AsEmpValid φ P.
+  as_emp_valid_0 : AsEmpValid φ P.
 Arguments AsEmpValid0 {_} _%type _%I.
-Existing Instance as_emp_valid_here | 0.
+Existing Instance as_emp_valid_0 | 0.
 
 Lemma as_emp_valid_1 (φ : Prop) {PROP : bi} (P : PROP) `{!AsEmpValid φ P} :
   φ → bi_emp_valid P.
-- 
GitLab