From fee229c17e6ff6bdf9cfc5679a0b6309f59fdedb Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Thu, 22 Dec 2016 10:51:58 +0100
Subject: [PATCH] core: fix typo in lemma name
---
theories/base_logic/lib/core.v | 2 +-
1 file changed, 1 insertion(+), 1 deletion(-)
diff --git a/theories/base_logic/lib/core.v b/theories/base_logic/lib/core.v
index 8d3663167..ba5de9b21 100644
--- a/theories/base_logic/lib/core.v
+++ b/theories/base_logic/lib/core.v
@@ -23,7 +23,7 @@ Section core.
iIntros (HPQ). iApply HQ. unshelve iApply ("HCP" $! Q). done.
Qed.
- Lemma corP_elim P : PersistentP P → coreP P -∗ P.
+ Lemma coreP_elim P : PersistentP P → coreP P -∗ P.
Proof.
iIntros (?) "HCP". unshelve iApply ("HCP" $! P). iIntros "P". done.
Qed.
--
GitLab