From e4091905d263458dd6f7a174217a787b8a1c8906 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Mon, 7 May 2018 23:57:02 +0200
Subject: [PATCH] Do not use automatically generated name.
---
theories/base_logic/upred.v | 2 +-
1 file changed, 1 insertion(+), 1 deletion(-)
diff --git a/theories/base_logic/upred.v b/theories/base_logic/upred.v
index 22c3b7f9a..2c628625d 100644
--- a/theories/base_logic/upred.v
+++ b/theories/base_logic/upred.v
@@ -509,7 +509,7 @@ Proof.
intros P Q.
unseal=> HP; split=>-[|n] x ??; [done|apply HP; eauto using cmra_validN_S].
- (* P ⊢ ▷ P *)
- intros P. unseal; split=> n x ? HP. destruct n; first done. simpl.
+ intros P. unseal; split=> -[|n] /= x ? HP; first done.
apply uPred_mono with (S n) x; eauto using cmra_validN_S.
- (* (∀ a, ▷ Φ a) ⊢ ▷ ∀ a, Φ a *)
intros A Φ. unseal; by split=> -[|n] x.
--
GitLab