From 52cc6b15fd6baf90101a33d96ad444248a48c506 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Thu, 11 Feb 2016 09:03:23 +0100
Subject: [PATCH] slightly simplify some proofs in upred.v

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

diff --git a/algebra/upred.v b/algebra/upred.v
index 08311e2c9..343dfccf3 100644
--- a/algebra/upred.v
+++ b/algebra/upred.v
@@ -341,13 +341,13 @@ Global Instance iff_proper :
 
 (** Introduction and elimination rules *)
 Lemma const_intro φ P : φ → P ⊑ ■ φ.
-Proof. by intros ?? [|?]. Qed.
+Proof. by intros ???. Qed.
 Lemma const_elim φ Q R : Q ⊑ ■ φ → (φ → Q ⊑ R) → Q ⊑ R.
 Proof. intros HQP HQR x n ??; apply HQR; first eapply (HQP _ n); eauto. Qed.
 Lemma True_intro P : P ⊑ True.
 Proof. by apply const_intro. Qed.
 Lemma False_elim P : False ⊑ P.
-Proof. by intros x [|n] ?. Qed.
+Proof. by intros x n ?. Qed.
 Lemma and_elim_l P Q : (P ∧ Q) ⊑ P.
 Proof. by intros x n ? [??]. Qed.
 Lemma and_elim_r P Q : (P ∧ Q) ⊑ Q.
-- 
GitLab