From 0135f46c2b2d344384abce6d6cef236ccc918e8a Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Wed, 23 Nov 2016 11:31:02 +0100
Subject: [PATCH] Eval hnf in iProof like in iPoseProof.

---
 proofmode/tactics.v | 10 +++++++---
 1 file changed, 7 insertions(+), 3 deletions(-)

diff --git a/proofmode/tactics.v b/proofmode/tactics.v
index ec00c04ab..331ec21eb 100644
--- a/proofmode/tactics.v
+++ b/proofmode/tactics.v
@@ -45,9 +45,13 @@ Ltac iMatchGoal tac :=
 Tactic Notation "iProof" :=
   lazymatch goal with
   | |- of_envs _ ⊢ _ => fail "iProof: already in Iris proofmode"
-  | |- True ⊢ _ => apply tac_adequate
-  | |- _ ⊢ _ => apply uPred.wand_entails, tac_adequate
-  | |- _ ⊣⊢ _ => apply uPred.iff_equiv, tac_adequate
+  | |- ?P =>
+    match eval hnf in P with
+    | True ⊢ _ => apply tac_adequate
+    | _ ⊢ _ => apply uPred.wand_entails, tac_adequate
+    (* need to use the unfolded version of [⊣⊢] due to the hnf *)
+    | uPred_equiv' _ _ => apply uPred.iff_equiv, tac_adequate
+    end
   end.
 
 (** * Context manipulation *)
-- 
GitLab