From 8f725f45cfad671ae00ba64db36126a25eab3da1 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Tue, 24 Apr 2018 15:30:23 +0200
Subject: [PATCH] use Lemma, not Let

---
 theories/tests/proofmode.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/theories/tests/proofmode.v b/theories/tests/proofmode.v
index a79341f8a..5bd5a79f3 100644
--- a/theories/tests/proofmode.v
+++ b/theories/tests/proofmode.v
@@ -115,7 +115,7 @@ Lemma test_iEmp_intro P Q R `{!Affine P, !Persistent Q, !Affine R} :
   P -∗ Q → R -∗ emp.
 Proof. iIntros "HP #HQ HR". iEmpIntro. Qed.
 
-Let test_fresh P Q:
+Lemma test_fresh P Q:
   (P ∗ Q) -∗ (P ∗ Q).
 Proof.
   iIntros "H".
-- 
GitLab