From 7c1a6c434b6e372440d258fe56812121ce8f8081 Mon Sep 17 00:00:00 2001
From: Jacques-Henri Jourdan <jacques-henri.jourdan@normalesup.org>
Date: Sun, 8 Sep 2019 22:58:10 +0200
Subject: [PATCH] NEw reference for tests.

---
 tests/proofmode_monpred.ref | 28 ++++++++++++++++++++++++++++
 1 file changed, 28 insertions(+)

diff --git a/tests/proofmode_monpred.ref b/tests/proofmode_monpred.ref
index 459ec829a..5b018493c 100644
--- a/tests/proofmode_monpred.ref
+++ b/tests/proofmode_monpred.ref
@@ -62,3 +62,31 @@ In nested Ltac calls to "iFrame (constr)",
 "<iris.proofmode.ltac_tactics.iFrame_go>" and
 "<iris.proofmode.ltac_tactics.iFrameHyp>", last call failed.
 Tactic failure: iFrame: cannot frame (P i).
+1 subgoal
+  
+  I : biIndex
+  Σ : gFunctors
+  invG0 : invG Σ
+  N : namespace
+  P : iProp Σ
+  ============================
+  "H" : ⎡ inv N (<pers> P) ⎤
+  "H2" : ⎡ ▷ <pers> P ⎤
+  --------------------------------------â–¡
+  |={⊤ ∖ ↑N}=> ⎡ ▷ <pers> P ⎤ ∗ (|={⊤}=> ⎡ ▷ P ⎤)
+  
+1 subgoal
+  
+  I : biIndex
+  Σ : gFunctors
+  invG0 : invG Σ
+  N : namespace
+  P : iProp Σ
+  ============================
+  "H" : ⎡ inv N (<pers> P) ⎤
+  "H2" : ⎡ ▷ <pers> P ⎤
+  --------------------------------------â–¡
+  "Hclose" : ⎡ ▷ <pers> P ={⊤ ∖ ↑N,⊤}=∗ emp ⎤
+  --------------------------------------∗
+  |={⊤ ∖ ↑N,⊤}=> ⎡ ▷ P ⎤
+  
-- 
GitLab