From 6415d82a4e23b4f0077a007ddde4e86f246dda53 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Thu, 18 Mar 2021 09:55:08 +0100
Subject: [PATCH] remove now stale .ref files

---
 tests/proofmode_ascii.8.11.ref   | 221 -------------------------------
 tests/proofmode_monpred.8.11.ref |  89 -------------
 2 files changed, 310 deletions(-)
 delete mode 100644 tests/proofmode_ascii.8.11.ref
 delete mode 100644 tests/proofmode_monpred.8.11.ref

diff --git a/tests/proofmode_ascii.8.11.ref b/tests/proofmode_ascii.8.11.ref
deleted file mode 100644
index 684c4232b..000000000
--- a/tests/proofmode_ascii.8.11.ref
+++ /dev/null
@@ -1,221 +0,0 @@
-1 goal
-  
-  Σ : gFunctors
-  invG0 : invG Σ
-  cinvG0 : cinvG Σ
-  na_invG0 : na_invG Σ
-  N : namespace
-  P : iProp Σ
-  ============================
-  "H" : inv N (<pers> P)
-  "H2" : â–· <pers> P
-  --------------------------------------â–¡
-  |={⊤ ∖ ↑N}=> ▷ <pers> P ∗ (|={⊤}=> ▷ P)
-  
-1 goal
-  
-  Σ : gFunctors
-  invG0 : invG Σ
-  cinvG0 : cinvG Σ
-  na_invG0 : na_invG Σ
-  N : namespace
-  P : iProp Σ
-  ============================
-  "H" : inv N (<pers> P)
-  "H2" : â–· <pers> P
-  --------------------------------------â–¡
-  "Hclose" : ▷ <pers> P ={⊤ ∖ ↑N,⊤}=∗ emp
-  --------------------------------------∗
-  |={⊤ ∖ ↑N,⊤}=> ▷ P
-  
-1 goal
-  
-  Σ : gFunctors
-  invG0 : invG Σ
-  cinvG0 : cinvG Σ
-  na_invG0 : na_invG Σ
-  γ : gname
-  p : Qp
-  N : namespace
-  P : iProp Σ
-  ============================
-  _ : cinv N γ (<pers> P)
-  "HP" : â–· <pers> P
-  --------------------------------------â–¡
-  "Hown" : cinv_own γ p
-  --------------------------------------∗
-  |={⊤ ∖ ↑N}=> ▷ <pers> P ∗ (|={⊤}=> cinv_own γ p ∗ ▷ P)
-  
-1 goal
-  
-  Σ : gFunctors
-  invG0 : invG Σ
-  cinvG0 : cinvG Σ
-  na_invG0 : na_invG Σ
-  γ : gname
-  p : Qp
-  N : namespace
-  P : iProp Σ
-  ============================
-  _ : cinv N γ (<pers> P)
-  "HP" : â–· <pers> P
-  --------------------------------------â–¡
-  "Hown" : cinv_own γ p
-  "Hclose" : ▷ <pers> P ={⊤ ∖ ↑N,⊤}=∗ emp
-  --------------------------------------∗
-  |={⊤ ∖ ↑N,⊤}=> cinv_own γ p ∗ ▷ P
-  
-1 goal
-  
-  Σ : gFunctors
-  invG0 : invG Σ
-  cinvG0 : cinvG Σ
-  na_invG0 : na_invG Σ
-  t : na_inv_pool_name
-  N : namespace
-  E1, E2 : coPset
-  P : iProp Σ
-  H : ↑N ⊆ E2
-  ============================
-  _ : na_inv t N (<pers> P)
-  "HP" : â–· <pers> P
-  --------------------------------------â–¡
-  "Hown1" : na_own t E1
-  "Hown2" : na_own t (E2 ∖ ↑N)
-  --------------------------------------∗
-  |={⊤}=> (▷ <pers> P ∗ na_own t (E2 ∖ ↑N))
-          ∗ (na_own t E2 ={⊤}=∗ na_own t E1 ∗ na_own t E2 ∗ ▷ P)
-  
-1 goal
-  
-  Σ : gFunctors
-  invG0 : invG Σ
-  cinvG0 : cinvG Σ
-  na_invG0 : na_invG Σ
-  t : na_inv_pool_name
-  N : namespace
-  E1, E2 : coPset
-  P : iProp Σ
-  H : ↑N ⊆ E2
-  ============================
-  _ : na_inv t N (<pers> P)
-  "HP" : â–· <pers> P
-  --------------------------------------â–¡
-  "Hown1" : na_own t E1
-  "Hown2" : na_own t (E2 ∖ ↑N)
-  "Hclose" : ▷ <pers> P ∗ na_own t (E2 ∖ ↑N) ={⊤}=∗ na_own t E2
-  --------------------------------------∗
-  |={⊤}=> na_own t E1 ∗ na_own t E2 ∗ ▷ P
-  
-"test_iInv_12"
-     : string
-The command has indeed failed with message:
-Tactic failure: iInv: selector 34 is not of the right type .
-The command has indeed failed with message:
-Tactic failure: iInv: invariant nroot not found.
-The command has indeed failed with message:
-Tactic failure: iInv: invariant "H2" not found.
-"test_iInv"
-     : string
-1 goal
-  
-  Σ : gFunctors
-  invG0 : invG Σ
-  I : biIndex
-  N : namespace
-  E : coPset
-  𝓟 : iProp Σ
-  H : ↑N ⊆ E
-  ============================
-  "HP" : ⎡ ▷ 𝓟 ⎤
-  --------------------------------------∗
-  |={E ∖ ↑N}=> ⎡ ▷ 𝓟 ⎤ ∗ (|={E}=> emp)
-  
-"test_iInv_with_close"
-     : string
-1 goal
-  
-  Σ : gFunctors
-  invG0 : invG Σ
-  I : biIndex
-  N : namespace
-  E : coPset
-  𝓟 : iProp Σ
-  H : ↑N ⊆ E
-  ============================
-  "HP" : ⎡ ▷ 𝓟 ⎤
-  "Hclose" : ⎡ ▷ 𝓟 ={E ∖ ↑N,E}=∗ emp ⎤
-  --------------------------------------∗
-  |={E ∖ ↑N,E}=> emp
-  
-"p1"
-     : string
-1 goal
-  
-  PROP : bi
-  ============================
-  forall (P : PROP) (_ : True), bi_entails P P
-"p2"
-     : string
-1 goal
-  
-  PROP : bi
-  ============================
-  forall P : PROP, and True (bi_entails P P)
-"p3"
-     : string
-1 goal
-  
-  PROP : bi
-  ============================
-  ex (fun P : PROP => bi_entails P P)
-"p4"
-     : string
-1 goal
-  
-  PROP : bi
-  ============================
-  bi_emp_valid (bi_exist (fun x : nat => bi_pure (eq x O)))
-"p5"
-     : string
-1 goal
-  
-  PROP : bi
-  ============================
-  bi_emp_valid (bi_exist (fun _ : nat => bi_pure (forall y : nat, eq y y)))
-"p6"
-     : string
-1 goal
-  
-  PROP : bi
-  ============================
-  ex
-    (unique
-       (fun z : nat =>
-        bi_emp_valid
-          (bi_exist
-             (fun _ : nat =>
-              bi_sep (bi_pure (forall y : nat, eq y y)) (bi_pure (eq z O))))))
-"p7"
-     : string
-1 goal
-  
-  PROP : bi
-  ============================
-  forall (a : nat) (_ : eq a O) (y : nat),
-  bi_entails (bi_pure True) (bi_pure (ge y O))
-"p8"
-     : string
-1 goal
-  
-  PROP : bi
-  ============================
-  forall (a : nat) (_ : eq a O) (y : nat), bi_emp_valid (bi_pure (ge y O))
-"p9"
-     : string
-1 goal
-  
-  PROP : bi
-  ============================
-  forall (a : nat) (_ : eq a O) (_ : nat),
-  bi_emp_valid (bi_forall (fun z : nat => bi_pure (ge z O)))
diff --git a/tests/proofmode_monpred.8.11.ref b/tests/proofmode_monpred.8.11.ref
deleted file mode 100644
index 2687a54f7..000000000
--- a/tests/proofmode_monpred.8.11.ref
+++ /dev/null
@@ -1,89 +0,0 @@
-1 goal
-  
-  I : biIndex
-  PROP : bi
-  P, Q : monPred
-  i : I
-  ============================
-  "HW" : (P -∗ Q) i
-  --------------------------------------∗
-  (P -∗ Q) i
-  
-1 goal
-  
-  I : biIndex
-  PROP : bi
-  P, Q : monPred
-  i, j : I
-  ============================
-  "HW" : (P -∗ Q) j
-  "HP" : P j
-  --------------------------------------∗
-  Q j
-  
-1 goal
-  
-  I : biIndex
-  PROP : bi
-  P, Q : monPred
-  Objective0 : Objective Q
-  𝓟, 𝓠 : PROP
-  ============================
-  "H2" : ∀ i : I, Q i
-  "H3" : 𝓟
-  "H4" : 𝓠
-  --------------------------------------∗
-  ∀ i : I, 𝓟 ∗ 𝓠 ∗ Q i
-  
-1 goal
-  
-  I : biIndex
-  PROP : bi
-  FU : BiFUpd PROP
-  P, Q : monPred
-  i : I
-  ============================
-  --------------------------------------∗
-  (Q -∗ emp) i
-  
-1 goal
-  
-  I : biIndex
-  PROP : bi
-  FU : BiFUpd PROP
-  P : monPred
-  i : I
-  ============================
-  --------------------------------------∗
-  ∀ _ : (), ∃ _ : (), emp
-  
-The command has indeed failed with message:
-Tactic failure: iFrame: cannot frame (P i).
-1 goal
-  
-  I : biIndex
-  Σ : gFunctors
-  invG0 : invG Σ
-  N : namespace
-  𝓟 : iProp Σ
-  ============================
-  "H" : ⎡ inv N (<pers> 𝓟) ⎤
-  "H2" : ⎡ ▷ <pers> 𝓟 ⎤
-  --------------------------------------â–¡
-  |={⊤ ∖ ↑N}=> ⎡ ▷ <pers> 𝓟 ⎤ ∗ (|={⊤}=> ⎡ ▷ 𝓟 ⎤)
-  
-1 goal
-  
-  I : biIndex
-  Σ : gFunctors
-  invG0 : invG Σ
-  N : namespace
-  𝓟 : iProp Σ
-  ============================
-  "H" : ⎡ inv N (<pers> 𝓟) ⎤
-  "H2" : ⎡ ▷ <pers> 𝓟 ⎤
-  --------------------------------------â–¡
-  "Hclose" : ⎡ ▷ <pers> 𝓟 ={⊤ ∖ ↑N,⊤}=∗ emp ⎤
-  --------------------------------------∗
-  |={⊤ ∖ ↑N,⊤}=> ⎡ ▷ 𝓟 ⎤
-  
-- 
GitLab