From 5eb59e133fde1a3e42b7c03c134d738b390df894 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Mon, 30 May 2016 13:25:12 +0200
Subject: [PATCH] Hint Resolve uPred.eq_refl'.
---
proofmode/tactics.v | 1 +
tests/proofmode.v | 4 ++--
2 files changed, 3 insertions(+), 2 deletions(-)
diff --git a/proofmode/tactics.v b/proofmode/tactics.v
index ed27be14a..119306c55 100644
--- a/proofmode/tactics.v
+++ b/proofmode/tactics.v
@@ -768,3 +768,4 @@ Tactic Notation "iRewrite" "-" open_constr(t) "in" constr(H) :=
(* Make sure that by and done solve trivial things in proof mode *)
Hint Extern 0 (of_envs _ ⊢ _) => by iPureIntro.
Hint Extern 0 (of_envs _ ⊢ _) => iAssumption.
+Hint Resolve uPred.eq_refl'. (* Maybe make an [iReflexivity] tactic *)
diff --git a/tests/proofmode.v b/tests/proofmode.v
index e82db494e..d0d7d4eec 100644
--- a/tests/proofmode.v
+++ b/tests/proofmode.v
@@ -67,9 +67,9 @@ Lemma demo_5 (M : ucmraT) (x y : M) (P : uPred M) :
(∀ z, P → z ≡ y) ⊢ (P -★ (x,x) ≡ (y,x)).
Proof.
iIntros "H1 H2".
- iRewrite (uPred.eq_sym x x with "[#]"). iApply uPred.eq_refl.
+ iRewrite (uPred.eq_sym x x with "[#]"); first done.
iRewrite -("H1" $! _ with "[#]"); first done.
- iApply uPred.eq_refl.
+ done.
Qed.
Lemma demo_6 (M : ucmraT) (P Q : uPred M) :
--
GitLab