diff --git a/test-normalizer.sed b/test-normalizer.sed
index b776836403723a8df4c41e87f998fc5848e1b817..ca19aad59b641c7c02166cf6d9801606f8b3aa45 100644
--- a/test-normalizer.sed
+++ b/test-normalizer.sed
@@ -1,2 +1,4 @@
 # adjust for https://github.com/coq/coq/pull/10239
 s/(simple_intropattern)/(intropattern)/g
+# adjust for https://github.com/coq/coq/pull/13656
+s/subgoal/goal/g
diff --git a/tests/atomic.ref b/tests/atomic.ref
index eb691fb7fadba8cba614547a193c1cf15b945e83..859bb6deb7e32902cf459b362c807d7e09ea45b6 100644
--- a/tests/atomic.ref
+++ b/tests/atomic.ref
@@ -1,4 +1,4 @@
-1 subgoal
+1 goal
   
   Σ : gFunctors
   heapG0 : heapG Σ
@@ -20,14 +20,14 @@ The command has indeed failed with message:
 Tactic failure: iAuIntro: not all spatial assumptions are laterable.
 "printing"
      : string
-1 subgoal
+1 goal
   
   Σ : gFunctors
   heapG0 : heapG Σ
   P : val → iProp Σ
   ============================
   ⊢ <<< ∀ x : val, P x >>> code @ ⊤ <<< ∃ y : val, P y, RET #() >>>
-1 subgoal
+1 goal
   
   Σ : gFunctors
   heapG0 : heapG Σ
@@ -38,7 +38,7 @@ Tactic failure: iAuIntro: not all spatial assumptions are laterable.
   --------------------------------------∗
   WP code {{ v, Φ v }}
   
-1 subgoal
+1 goal
   
   Σ : gFunctors
   heapG0 : heapG Σ
@@ -52,14 +52,14 @@ Tactic failure: iAuIntro: not all spatial assumptions are laterable.
   --------------------------------------∗
   WP code {{ v, Φ v }}
   
-1 subgoal
+1 goal
   
   Σ : gFunctors
   heapG0 : heapG Σ
   l : loc
   ============================
   ⊢ <<< ∀ x : val, l ↦ x >>> code @ ⊤ <<< l ↦ x, RET #() >>>
-1 subgoal
+1 goal
   
   Σ : gFunctors
   heapG0 : heapG Σ
@@ -70,7 +70,7 @@ Tactic failure: iAuIntro: not all spatial assumptions are laterable.
   --------------------------------------∗
   WP code {{ v, Φ v }}
   
-1 subgoal
+1 goal
   
   Σ : gFunctors
   heapG0 : heapG Σ
@@ -83,14 +83,14 @@ Tactic failure: iAuIntro: not all spatial assumptions are laterable.
   --------------------------------------∗
   WP code {{ v, Φ v }}
   
-1 subgoal
+1 goal
   
   Σ : gFunctors
   heapG0 : heapG Σ
   l : loc
   ============================
   ⊢ <<< l ↦ #() >>> code @ ⊤ <<< ∃ y : val, l ↦ y, RET #() >>>
-1 subgoal
+1 goal
   
   Σ : gFunctors
   heapG0 : heapG Σ
@@ -101,7 +101,7 @@ Tactic failure: iAuIntro: not all spatial assumptions are laterable.
   --------------------------------------∗
   WP code {{ v, Φ v }}
   
-1 subgoal
+1 goal
   
   Σ : gFunctors
   heapG0 : heapG Σ
@@ -115,14 +115,14 @@ Tactic failure: iAuIntro: not all spatial assumptions are laterable.
   --------------------------------------∗
   WP code {{ v, Φ v }}
   
-1 subgoal
+1 goal
   
   Σ : gFunctors
   heapG0 : heapG Σ
   l : loc
   ============================
   ⊢ <<< l ↦ #() >>> code @ ⊤ <<< l ↦ #(), RET #() >>>
-1 subgoal
+1 goal
   
   Σ : gFunctors
   heapG0 : heapG Σ
@@ -133,7 +133,7 @@ Tactic failure: iAuIntro: not all spatial assumptions are laterable.
   --------------------------------------∗
   WP code {{ v, Φ v }}
   
-1 subgoal
+1 goal
   
   Σ : gFunctors
   heapG0 : heapG Σ
@@ -148,7 +148,7 @@ Tactic failure: iAuIntro: not all spatial assumptions are laterable.
   
 "Now come the long pre/post tests"
      : string
-1 subgoal
+1 goal
   
   Σ : gFunctors
   heapG0 : heapG Σ
@@ -157,7 +157,7 @@ Tactic failure: iAuIntro: not all spatial assumptions are laterable.
   ⊢ <<< ∀ x : val, l ↦ x ∗ l ↦ x >>>
       code @ ⊤
     <<< ∃ y : val, l ↦ y, RET #() >>>
-1 subgoal
+1 goal
   
   Σ : gFunctors
   heapG0 : heapG Σ
@@ -169,7 +169,7 @@ Tactic failure: iAuIntro: not all spatial assumptions are laterable.
   --------------------------------------∗
   WP code {{ v, Φ v }}
   
-1 subgoal
+1 goal
   
   Σ : gFunctors
   heapG0 : heapG Σ
@@ -178,7 +178,7 @@ Tactic failure: iAuIntro: not all spatial assumptions are laterable.
   ⊢ <<< ∀ x : val, l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x >>>
       code @ ⊤
     <<< ∃ y : val, l ↦ y, RET #() >>>
-1 subgoal
+1 goal
   
   Σ : gFunctors
   heapG0 : heapG Σ
@@ -190,7 +190,7 @@ Tactic failure: iAuIntro: not all spatial assumptions are laterable.
   --------------------------------------∗
   WP code {{ v, Φ v }}
   
-1 subgoal
+1 goal
   
   Σ : gFunctors
   heapG0 : heapG Σ
@@ -200,7 +200,7 @@ Tactic failure: iAuIntro: not all spatial assumptions are laterable.
       code @ ⊤
     <<< ∃ yyyy : val, l ↦ yyyy ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx,
         RET #() >>>
-1 subgoal
+1 goal
   
   Σ : gFunctors
   heapG0 : heapG Σ
@@ -214,7 +214,7 @@ Tactic failure: iAuIntro: not all spatial assumptions are laterable.
   --------------------------------------∗
   WP code {{ v, Φ v }}
   
-1 subgoal
+1 goal
   
   Σ : gFunctors
   heapG0 : heapG Σ
@@ -223,7 +223,7 @@ Tactic failure: iAuIntro: not all spatial assumptions are laterable.
   ⊢ <<< ∀ x : val, l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x >>>
       code @ ⊤
     <<< l ↦ x, RET #() >>>
-1 subgoal
+1 goal
   
   Σ : gFunctors
   heapG0 : heapG Σ
@@ -235,7 +235,7 @@ Tactic failure: iAuIntro: not all spatial assumptions are laterable.
   --------------------------------------∗
   WP code {{ v, Φ v }}
   
-1 subgoal
+1 goal
   
   Σ : gFunctors
   heapG0 : heapG Σ
@@ -245,7 +245,7 @@ Tactic failure: iAuIntro: not all spatial assumptions are laterable.
   ⊢ <<< l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x >>>
       code @ ⊤
     <<< ∃ y : val, l ↦ y, RET #() >>>
-1 subgoal
+1 goal
   
   Σ : gFunctors
   heapG0 : heapG Σ
@@ -258,7 +258,7 @@ Tactic failure: iAuIntro: not all spatial assumptions are laterable.
   --------------------------------------∗
   WP code {{ v, Φ v }}
   
-1 subgoal
+1 goal
   
   Σ : gFunctors
   heapG0 : heapG Σ
@@ -268,7 +268,7 @@ Tactic failure: iAuIntro: not all spatial assumptions are laterable.
   ⊢ <<< l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x >>>
       code @ ⊤
     <<< l ↦ #(), RET #() >>>
-1 subgoal
+1 goal
   
   Σ : gFunctors
   heapG0 : heapG Σ
@@ -281,7 +281,7 @@ Tactic failure: iAuIntro: not all spatial assumptions are laterable.
   --------------------------------------∗
   WP code {{ v, Φ v }}
   
-1 subgoal
+1 goal
   
   Σ : gFunctors
   heapG0 : heapG Σ
@@ -291,7 +291,7 @@ Tactic failure: iAuIntro: not all spatial assumptions are laterable.
   ⊢ <<< l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx >>>
       code @ ⊤
     <<< l ↦ yyyy, RET #() >>>
-1 subgoal
+1 goal
   
   Σ : gFunctors
   heapG0 : heapG Σ
@@ -304,7 +304,7 @@ Tactic failure: iAuIntro: not all spatial assumptions are laterable.
   --------------------------------------∗
   WP code {{ v, Φ v }}
   
-1 subgoal
+1 goal
   
   Σ : gFunctors
   heapG0 : heapG Σ
@@ -315,7 +315,7 @@ Tactic failure: iAuIntro: not all spatial assumptions are laterable.
       code @ ⊤
     <<< l ↦ yyyy ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx,
         RET #() >>>
-1 subgoal
+1 goal
   
   Σ : gFunctors
   heapG0 : heapG Σ
@@ -331,7 +331,7 @@ Tactic failure: iAuIntro: not all spatial assumptions are laterable.
   
 "Prettification"
      : string
-1 subgoal
+1 goal
   
   Σ : gFunctors
   heapG0 : heapG Σ
diff --git a/tests/heap_lang.ref b/tests/heap_lang.ref
index 784aad7a5d476affff351ff603bfc716ca77637a..776a2e02e12a98839318814992cea8f932ac1786 100644
--- a/tests/heap_lang.ref
+++ b/tests/heap_lang.ref
@@ -1,6 +1,6 @@
 "heap_e_spec"
      : string
-1 subgoal
+1 goal
   
   Σ : gFunctors
   heapG0 : heapG Σ
@@ -9,7 +9,7 @@
   --------------------------------------∗
   WP let: "x" := ref #1 in "x" <- ! "x" + #1;; ! "x" @ E {{ v, ⌜v = #2⌝ }}
   
-1 subgoal
+1 goal
   
   Σ : gFunctors
   heapG0 : heapG Σ
@@ -22,7 +22,7 @@
   
 "heap_e2_spec"
      : string
-1 subgoal
+1 goal
   
   Σ : gFunctors
   heapG0 : heapG Σ
@@ -34,7 +34,7 @@
   WP let: "x" := #l in let: "y" := ref #1 in "x" <- ! "x" + #1;; ! "x"
   @ E [{ v, ⌜v = #2⌝ }]
   
-1 subgoal
+1 goal
   
   Σ : gFunctors
   heapG0 : heapG Σ
@@ -48,7 +48,7 @@
   
 "heap_e7_spec"
      : string
-1 subgoal
+1 goal
   
   Σ : gFunctors
   heapG0 : heapG Σ
@@ -58,7 +58,7 @@
   --------------------------------------∗
   WP CmpXchg #l #0 #1 {{ _, l ↦ #1 }}
   
-1 subgoal
+1 goal
   
   Σ : gFunctors
   heapG0 : heapG Σ
@@ -68,7 +68,7 @@
   --------------------------------------∗
   |={⊤}=> l ↦ #1
   
-1 subgoal
+1 goal
   
   Σ : gFunctors
   heapG0 : heapG Σ
@@ -79,7 +79,7 @@
   --------------------------------------∗
   |={⊤}=> True
   
-1 subgoal
+1 goal
   
   Σ : gFunctors
   heapG0 : heapG Σ
@@ -93,7 +93,7 @@
 The command has indeed failed with message:
 Tactic failure: wp_pure: cannot find ?y in (Var "x") or 
 ?y is not a redex.
-1 subgoal
+1 goal
   
   Σ : gFunctors
   heapG0 : heapG Σ
@@ -101,7 +101,7 @@ Tactic failure: wp_pure: cannot find ?y in (Var "x") or
   --------------------------------------∗
   WP "x" {{ _, True }}
   
-1 subgoal
+1 goal
   
   Σ : gFunctors
   heapG0 : heapG Σ
@@ -117,7 +117,7 @@ Tactic failure: wp_pure: cannot find ?y in (Var "x") or
   
 "test_array_fraction_destruct"
      : string
-1 subgoal
+1 goal
   
   Σ : gFunctors
   heapG0 : heapG Σ
@@ -131,7 +131,7 @@ Tactic failure: wp_pure: cannot find ?y in (Var "x") or
   
 "test_wp_finish_fupd"
      : string
-1 subgoal
+1 goal
   
   Σ : gFunctors
   heapG0 : heapG Σ
@@ -142,7 +142,7 @@ Tactic failure: wp_pure: cannot find ?y in (Var "x") or
   
 "test_twp_finish_fupd"
      : string
-1 subgoal
+1 goal
   
   Σ : gFunctors
   heapG0 : heapG Σ
@@ -151,7 +151,7 @@ Tactic failure: wp_pure: cannot find ?y in (Var "x") or
   --------------------------------------∗
   |={⊤}=> True
   
-1 subgoal
+1 goal
   
   Σ : gFunctors
   heapG0 : heapG Σ
@@ -165,7 +165,7 @@ Tactic failure: wp_pure: cannot find ?y in (Var "x") or
   --------------------------------------∗
   WP ! #l {{ v, Φ v }}
   
-1 subgoal
+1 goal
   
   Σ : gFunctors
   heapG0 : heapG Σ
@@ -179,7 +179,7 @@ Tactic failure: wp_pure: cannot find ?y in (Var "x") or
   --------------------------------------∗
   WP ! #l [{ v, Φ v }]
   
-1 subgoal
+1 goal
   
   Σ : gFunctors
   heapG0 : heapG Σ
@@ -190,7 +190,7 @@ Tactic failure: wp_pure: cannot find ?y in (Var "x") or
   ⊢ l ↦_(λ _ : val, I #true) □
 "wp_iMod_fupd_atomic"
      : string
-2 subgoals
+2 goals
   
   Σ : gFunctors
   heapG0 : heapG Σ
@@ -199,14 +199,14 @@ Tactic failure: wp_pure: cannot find ?y in (Var "x") or
   ============================
   Atomic (stuckness_to_atomicity NotStuck) (#() #())
 
-subgoal 2 is:
+goal 2 is:
  "H" : P
 --------------------------------------∗
 WP #() #() @ E2 {{ _, |={E2,E1}=> True }}
 
 "wp_iInv_atomic"
      : string
-2 subgoals
+2 goals
   
   Σ : gFunctors
   heapG0 : heapG Σ
@@ -217,7 +217,7 @@ WP #() #() @ E2 {{ _, |={E2,E1}=> True }}
   ============================
   Atomic (stuckness_to_atomicity NotStuck) (#() #())
 
-subgoal 2 is:
+goal 2 is:
  "H" : â–· P
 "Hclose" : ▷ P ={E ∖ ↑N,E}=∗ emp
 --------------------------------------∗
@@ -225,7 +225,7 @@ WP #() #() @ E ∖ ↑N {{ _, |={E ∖ ↑N,E}=> True }}
 
 "wp_iInv_atomic_acc"
      : string
-2 subgoals
+2 goals
   
   Σ : gFunctors
   heapG0 : heapG Σ
@@ -236,12 +236,12 @@ WP #() #() @ E ∖ ↑N {{ _, |={E ∖ ↑N,E}=> True }}
   ============================
   Atomic (stuckness_to_atomicity NotStuck) (#() #())
 
-subgoal 2 is:
+goal 2 is:
  "H" : â–· P
 --------------------------------------∗
 WP #() #() @ E ∖ ↑N {{ _, |={E ∖ ↑N}=> ▷ P ∗ True }}
 
-1 subgoal
+1 goal
   
   Σ : gFunctors
   heapG0 : heapG Σ
@@ -249,7 +249,7 @@ WP #() #() @ E ∖ ↑N {{ _, |={E ∖ ↑N}=> ▷ P ∗ True }}
   --------------------------------------∗
   WP let: "f" := λ: "x", "x" in ref ("f" #10) {{ _, True }}
   
-1 subgoal
+1 goal
   
   Σ : gFunctors
   heapG0 : heapG Σ
@@ -261,7 +261,7 @@ WP #() #() @ E ∖ ↑N {{ _, |={E ∖ ↑N}=> ▷ P ∗ True }}
      let: "val3" := fun3 "val2" in if: "val1" = "val2" then "val" else "val3"
   {{ _, True }}
   
-1 subgoal
+1 goal
   
   Σ : gFunctors
   heapG0 : heapG Σ
@@ -274,7 +274,7 @@ WP #() #() @ E ∖ ↑N {{ _, |={E ∖ ↑N}=> ▷ P ∗ True }}
      let: "v" := fun3 "v" in if: "v" = "v" then "v" else "v" 
   {{ v, Φ v }}
   
-1 subgoal
+1 goal
   
   Σ : gFunctors
   heapG0 : heapG Σ
@@ -288,7 +288,7 @@ WP #() #() @ E ∖ ↑N {{ _, |={E ∖ ↑N}=> ▷ P ∗ True }}
      let: "v" := fun3 "v" in if: "v" = "v" then "v" else "v" 
   @ E {{ v, Φ v }}
   
-1 subgoal
+1 goal
   
   Σ : gFunctors
   heapG0 : heapG Σ
diff --git a/tests/heap_lang2.ref b/tests/heap_lang2.ref
index b21642a0e1a96a6609de640e70a958c401508a6f..dff62fa87c541d8a9c6fd3ef8e0197c946d5bf88 100644
--- a/tests/heap_lang2.ref
+++ b/tests/heap_lang2.ref
@@ -1,11 +1,11 @@
-1 subgoal
+1 goal
   
   Σ : gFunctors
   heapG0 : heapG Σ
   P, Q : iProp Σ
   ============================
   P ={⊤}=∗ Q
-1 subgoal
+1 goal
   
   Σ : gFunctors
   heapG0 : heapG Σ
@@ -17,7 +17,7 @@
      let: "val3" := fun3 "val2" in if: "val1" = "val2" then "val" else "val3"
   {{ _, True }}
   
-1 subgoal
+1 goal
   
   Σ : gFunctors
   heapG0 : heapG Σ
diff --git a/tests/ipm_paper.ref b/tests/ipm_paper.ref
index 486e79dd063618065ce99a0a2518d25471d59fa9..aa78bae6c40d2a44bfebc8b2328bd96763540102 100644
--- a/tests/ipm_paper.ref
+++ b/tests/ipm_paper.ref
@@ -1,6 +1,6 @@
 "sep_exist"
      : string
-1 subgoal
+1 goal
   
   M : ucmraT
   A : Type
@@ -14,7 +14,7 @@
   --------------------------------------∗
   Ψ x ∗ P
   
-2 subgoals
+2 goals
   
   M : ucmraT
   A : Type
@@ -27,13 +27,13 @@
   Ψ x
   
 
-subgoal 2 is:
+goal 2 is:
  "HP" : P
 "HR" : R
 --------------------------------------∗
 P
 
-1 subgoal
+1 goal
   
   M : ucmraT
   A : Type
@@ -48,7 +48,7 @@ P
   
 "sep_exist_short"
      : string
-1 subgoal
+1 goal
   
   M : ucmraT
   A : Type
@@ -63,7 +63,7 @@ P
   
 "read_spec"
      : string
-1 subgoal
+1 goal
   
   Σ : gFunctors
   heapG0 : heapG Σ
@@ -79,7 +79,7 @@ P
   --------------------------------------∗
   WP ! #l {{ v, ∃ m : nat, ⌜v = #m ∧ n ≤ m⌝ ∧ C l m }}
   
-1 subgoal
+1 goal
   
   Σ : gFunctors
   heapG0 : heapG Σ
diff --git a/tests/list_reverse.ref b/tests/list_reverse.ref
index 9440658dbf4e4d8b3cefd1c3f2577fc1afb222fd..b92601d2c985bc7b8030798397c05f7b8be60bac 100644
--- a/tests/list_reverse.ref
+++ b/tests/list_reverse.ref
@@ -1,4 +1,4 @@
-1 subgoal
+1 goal
   
   Σ : gFunctors
   heapG0 : heapG Σ
@@ -12,7 +12,7 @@
   --------------------------------------∗
   WP rev hd acc [{ v, Φ v }]
   
-1 subgoal
+1 goal
   
   Σ : gFunctors
   heapG0 : heapG Σ
diff --git a/tests/mosel_paper.ref b/tests/mosel_paper.ref
index 700e1159a429303df2d04f7dd27d6ef515796122..0369dfe162820419ade5167b99d35330ae1bb269 100644
--- a/tests/mosel_paper.ref
+++ b/tests/mosel_paper.ref
@@ -1,4 +1,4 @@
-1 subgoal
+1 goal
   
   PROP : bi
   A : Type
@@ -10,7 +10,7 @@
   --------------------------------------∗
   ∃ a : A, P ∗ Φ a ∨ P ∗ Ψ a
   
-1 subgoal
+1 goal
   
   PROP : bi
   A : Type
@@ -23,7 +23,7 @@
   --------------------------------------∗
   ∃ a : A, P ∗ Φ a ∨ P ∗ Ψ a
   
-1 subgoal
+1 goal
   
   PROP : bi
   A : Type
@@ -36,7 +36,7 @@
   --------------------------------------∗
   ∃ a : A, P ∗ Φ a ∨ P ∗ Ψ a
   
-1 subgoal
+1 goal
   
   PROP : bi
   A : Type
@@ -48,7 +48,7 @@
   --------------------------------------∗
   ∃ a : A, P ∗ Φ a ∨ P ∗ Ψ a
   
-1 subgoal
+1 goal
   
   PROP : bi
   A : Type
@@ -59,7 +59,7 @@
   --------------------------------------∗
   ∃ x : A, Φ x ∨ Ψ x
   
-1 subgoal
+1 goal
   
   PROP : bi
   A : Type
@@ -72,7 +72,7 @@
   --------------------------------------∗
   Φ x
   
-1 subgoal
+1 goal
   
   PROP : bi
   A : Type
@@ -85,7 +85,7 @@
   --------------------------------------∗
   P ∗ Ψ x
   
-1 subgoal
+1 goal
   
   PROP : bi
   A : Type
@@ -98,7 +98,7 @@
   --------------------------------------∗
   ∃ a : A, Φ a ∨ P ∗ P ∗ Ψ a
   
-1 subgoal
+1 goal
   
   PROP : bi
   A : Type
@@ -112,7 +112,7 @@
   --------------------------------------∗
   P ∗ P ∗ Ψ x
   
-1 subgoal
+1 goal
   
   PROP : bi
   A : Type
@@ -123,7 +123,7 @@
   --------------------------------------â–¡
   □ (P ∗ Q)
   
-1 subgoal
+1 goal
   
   I : biIndex
   PROP : bi
@@ -134,7 +134,7 @@
   --------------------------------------∗
   Ψ
   
-1 subgoal
+1 goal
   
   I : biIndex
   PROP : bi
@@ -143,7 +143,7 @@
   --------------------------------------∗
   ∀ i : I, Φ i ∗ (Φ -∗ Ψ) i -∗ Ψ i
   
-1 subgoal
+1 goal
   
   I : biIndex
   PROP : bi
@@ -157,7 +157,7 @@
   --------------------------------------∗
   ⎡ P ∗ Q ⎤
   
-1 subgoal
+1 goal
   
   I : biIndex
   PROP : bi
diff --git a/tests/one_shot.ref b/tests/one_shot.ref
index c06e1621c61a96598a4f9583800380f048216bfa..182ac473defb6f95ccc9eee57e01c738df35bc55 100644
--- a/tests/one_shot.ref
+++ b/tests/one_shot.ref
@@ -1,4 +1,4 @@
-1 subgoal
+1 goal
   
   Σ : gFunctors
   heapG0 : heapG Σ
@@ -17,7 +17,7 @@
   ∗ (⌜InjLV #() = InjLV #()⌝
      ∨ (∃ n : Z, ⌜InjLV #() = InjRV #n⌝ ∗ own γ (Shot n)))
   
-1 subgoal
+1 goal
   
   Σ : gFunctors
   heapG0 : heapG Σ
diff --git a/tests/one_shot_once.ref b/tests/one_shot_once.ref
index 58301394b7a870f24581635d859d10138fbafb2b..686937f1065150df00ae611d3f68801822a9a8bf 100644
--- a/tests/one_shot_once.ref
+++ b/tests/one_shot_once.ref
@@ -1,4 +1,4 @@
-1 subgoal
+1 goal
   
   Σ : gFunctors
   heapG0 : heapG Σ
@@ -17,7 +17,7 @@
   ∗ (⌜InjLV #() = InjLV #()⌝
      ∨ (∃ n : Z, ⌜InjLV #() = InjRV #n⌝ ∗ own γ (Shot n)))
   
-1 subgoal
+1 goal
   
   Σ : gFunctors
   heapG0 : heapG Σ
diff --git a/tests/proofmode.ref b/tests/proofmode.ref
index ba95cf6eafae0a4381f282779d438d22e936cb63..bae7935704c71df35a2c3e757c5b70def5bd6b6b 100644
--- a/tests/proofmode.ref
+++ b/tests/proofmode.ref
@@ -1,6 +1,6 @@
 "demo_0"
      : string
-1 subgoal
+1 goal
   
   PROP : bi
   P, Q : PROP
@@ -11,7 +11,7 @@
   --------------------------------------∗
   Q ∨ P
   
-1 subgoal
+1 goal
   
   PROP : bi
   P, Q : PROP
@@ -23,7 +23,7 @@
   
 "test_iStopProof"
      : string
-1 subgoal
+1 goal
   
   PROP : bi
   Q : PROP
@@ -34,7 +34,7 @@
   --------------------------------------∗
   Q
   
-1 subgoal
+1 goal
   
   PROP : bi
   Q : PROP
@@ -42,7 +42,7 @@
   □ emp ∗ Q -∗ Q
 "test_iDestruct_and_emp"
      : string
-1 subgoal
+1 goal
   
   PROP : bi
   P, Q : PROP
@@ -56,7 +56,7 @@
   
 "test_iDestruct_spatial"
      : string
-1 subgoal
+1 goal
   
   PROP : bi
   Q : PROP
@@ -67,7 +67,7 @@
   
 "test_iDestruct_spatial_affine"
      : string
-1 subgoal
+1 goal
   
   PROP : bi
   Q : PROP
@@ -83,7 +83,7 @@ The command has indeed failed with message:
 Tactic failure: iExistDestruct: cannot destruct P.
 "test_iDestruct_exists_intuitionistic"
      : string
-1 subgoal
+1 goal
   
   PROP : bi
   P : PROP
@@ -96,7 +96,7 @@ Tactic failure: iExistDestruct: cannot destruct P.
   
 "test_iDestruct_exists_anonymous"
      : string
-1 subgoal
+1 goal
   
   PROP : bi
   P : PROP
@@ -109,7 +109,7 @@ Tactic failure: iExistDestruct: cannot destruct P.
   
 "test_iIntros_forall_pure"
      : string
-1 subgoal
+1 goal
   
   PROP : bi
   Ψ : nat → PROP
@@ -120,7 +120,7 @@ Tactic failure: iExistDestruct: cannot destruct P.
   
 "test_iIntros_pure_names"
      : string
-1 subgoal
+1 goal
   
   PROP : bi
   H : True
@@ -162,7 +162,7 @@ The command has indeed failed with message:
 Tactic failure: iSpecialize: cannot instantiate (⌜φ⌝ → P -∗ False)%I with P.
 "test_iNext_plus_3"
      : string
-1 subgoal
+1 goal
   
   PROP : bi
   P, Q : PROP
@@ -173,7 +173,7 @@ Tactic failure: iSpecialize: cannot instantiate (⌜φ⌝ → P -∗ False)%I wi
   
 "test_specialize_nested_intuitionistic"
      : string
-1 subgoal
+1 goal
   
   PROP : bi
   φ : Prop
@@ -189,7 +189,7 @@ Tactic failure: iSpecialize: cannot instantiate (⌜φ⌝ → P -∗ False)%I wi
   
 "test_iSimpl_in"
      : string
-1 subgoal
+1 goal
   
   PROP : bi
   x, y : nat
@@ -198,7 +198,7 @@ Tactic failure: iSpecialize: cannot instantiate (⌜φ⌝ → P -∗ False)%I wi
   --------------------------------------∗
   ⌜S (S (S x)) = y⌝
   
-1 subgoal
+1 goal
   
   PROP : bi
   x, y, z : nat
@@ -208,7 +208,7 @@ Tactic failure: iSpecialize: cannot instantiate (⌜φ⌝ → P -∗ False)%I wi
   --------------------------------------∗
   ⌜S (S (S x)) = y⌝
   
-1 subgoal
+1 goal
   
   PROP : bi
   x, y, z : nat
@@ -225,7 +225,7 @@ The command has indeed failed with message:
 Tactic failure: iEval: %: unsupported selection pattern.
 "test_iFrame_later_1"
      : string
-1 subgoal
+1 goal
   
   PROP : bi
   P, Q : PROP
@@ -235,7 +235,7 @@ Tactic failure: iEval: %: unsupported selection pattern.
   
 "test_iFrame_later_2"
      : string
-1 subgoal
+1 goal
   
   PROP : bi
   P, Q : PROP
@@ -247,7 +247,7 @@ The command has indeed failed with message:
 Tactic failure: iFrame: cannot frame Q.
 "test_and_sep_affine_bi"
      : string
-1 subgoal
+1 goal
   
   PROP : bi
   BiAffine0 : BiAffine PROP
@@ -260,7 +260,7 @@ Tactic failure: iFrame: cannot frame Q.
   
 "test_big_sepL_simpl"
      : string
-1 subgoal
+1 goal
   
   PROP : bi
   x : nat
@@ -273,7 +273,7 @@ Tactic failure: iFrame: cannot frame Q.
   --------------------------------------∗
   P
   
-1 subgoal
+1 goal
   
   PROP : bi
   x : nat
@@ -288,7 +288,7 @@ Tactic failure: iFrame: cannot frame Q.
   
 "test_big_sepL2_simpl"
      : string
-1 subgoal
+1 goal
   
   PROP : bi
   x1, x2 : nat
@@ -301,7 +301,7 @@ Tactic failure: iFrame: cannot frame Q.
   --------------------------------------∗
   P ∨ ([∗ list] _;_ ∈ (x1 :: l1);(x2 :: l2), True)
   
-1 subgoal
+1 goal
   
   PROP : bi
   x1, x2 : nat
@@ -317,7 +317,7 @@ Tactic failure: iFrame: cannot frame Q.
   
 "test_big_sepL2_iDestruct"
      : string
-1 subgoal
+1 goal
   
   PROP : bi
   Φ : nat → nat → PROP
@@ -331,7 +331,7 @@ Tactic failure: iFrame: cannot frame Q.
   
 "test_reducing_after_iDestruct"
      : string
-1 subgoal
+1 goal
   
   PROP : bi
   ============================
@@ -341,7 +341,7 @@ Tactic failure: iFrame: cannot frame Q.
   
 "test_reducing_after_iApply"
      : string
-1 subgoal
+1 goal
   
   PROP : bi
   ============================
@@ -351,7 +351,7 @@ Tactic failure: iFrame: cannot frame Q.
   
 "test_reducing_after_iApply_late_evar"
      : string
-1 subgoal
+1 goal
   
   PROP : bi
   ============================
@@ -361,7 +361,7 @@ Tactic failure: iFrame: cannot frame Q.
   
 "test_wandM"
      : string
-1 subgoal
+1 goal
   
   PROP : bi
   mP : option PROP
@@ -373,7 +373,7 @@ Tactic failure: iFrame: cannot frame Q.
   --------------------------------------∗
   R
   
-1 subgoal
+1 goal
   
   PROP : bi
   mP : option PROP
@@ -385,7 +385,7 @@ Tactic failure: iFrame: cannot frame Q.
   
 "elim_mod_accessor"
      : string
-1 subgoal
+1 goal
   
   PROP : bi
   BiFUpd0 : BiFUpd PROP
@@ -400,7 +400,7 @@ Tactic failure: iFrame: cannot frame Q.
   
 "print_long_line_1"
      : string
-1 subgoal
+1 goal
   
   PROP : bi
   BiFUpd0 : BiFUpd PROP
@@ -411,7 +411,7 @@ Tactic failure: iFrame: cannot frame Q.
   --------------------------------------∗
   True
   
-1 subgoal
+1 goal
   
   PROP : bi
   BiFUpd0 : BiFUpd PROP
@@ -424,7 +424,7 @@ Tactic failure: iFrame: cannot frame Q.
   
 "print_long_line_2"
      : string
-1 subgoal
+1 goal
   
   PROP : bi
   BiFUpd0 : BiFUpd PROP
@@ -435,7 +435,7 @@ Tactic failure: iFrame: cannot frame Q.
   --------------------------------------∗
   True
   
-1 subgoal
+1 goal
   
   PROP : bi
   BiFUpd0 : BiFUpd PROP
@@ -448,7 +448,7 @@ Tactic failure: iFrame: cannot frame Q.
   
 "long_impl"
      : string
-1 subgoal
+1 goal
   
   PROP : bi
   BiFUpd0 : BiFUpd PROP
@@ -460,7 +460,7 @@ Tactic failure: iFrame: cannot frame Q.
   
 "long_impl_nested"
      : string
-1 subgoal
+1 goal
   
   PROP : bi
   BiFUpd0 : BiFUpd PROP
@@ -473,7 +473,7 @@ Tactic failure: iFrame: cannot frame Q.
   
 "long_wand"
      : string
-1 subgoal
+1 goal
   
   PROP : bi
   BiFUpd0 : BiFUpd PROP
@@ -485,7 +485,7 @@ Tactic failure: iFrame: cannot frame Q.
   
 "long_wand_nested"
      : string
-1 subgoal
+1 goal
   
   PROP : bi
   BiFUpd0 : BiFUpd PROP
@@ -498,7 +498,7 @@ Tactic failure: iFrame: cannot frame Q.
   
 "long_fupd"
      : string
-1 subgoal
+1 goal
   
   PROP : bi
   BiFUpd0 : BiFUpd PROP
@@ -511,7 +511,7 @@ Tactic failure: iFrame: cannot frame Q.
   
 "long_fupd_nested"
      : string
-1 subgoal
+1 goal
   
   PROP : bi
   BiFUpd0 : BiFUpd PROP
@@ -709,7 +709,7 @@ The command has indeed failed with message:
 Tactic failure: iLöb: no 'BiLöb' instance found.
 "test_pure_name"
      : string
-1 subgoal
+1 goal
   
   PROP : bi
   P : PROP
diff --git a/tests/proofmode_ascii.ref b/tests/proofmode_ascii.ref
index ca5a2760305f617d2345996fd1967835570f188d..6c4fc6ad6fd4fb1001b0273627b8c254c91355cc 100644
--- a/tests/proofmode_ascii.ref
+++ b/tests/proofmode_ascii.ref
@@ -1,4 +1,4 @@
-1 subgoal
+1 goal
   
   Σ : gFunctors
   invG0 : invG Σ
@@ -12,7 +12,7 @@
   --------------------------------------â–¡
   |={⊤ ∖ ↑N}=> ▷ <pers> P ∗ (|={⊤}=> ▷ P)
   
-1 subgoal
+1 goal
   
   Σ : gFunctors
   invG0 : invG Σ
@@ -28,7 +28,7 @@
   --------------------------------------∗
   |={⊤ ∖ ↑N,⊤}=> ▷ P
   
-1 subgoal
+1 goal
   
   Σ : gFunctors
   invG0 : invG Σ
@@ -46,7 +46,7 @@
   --------------------------------------∗
   |={⊤ ∖ ↑N}=> ▷ <pers> P ∗ (|={⊤}=> cinv_own γ p ∗ ▷ P)
   
-1 subgoal
+1 goal
   
   Σ : gFunctors
   invG0 : invG Σ
@@ -65,7 +65,7 @@
   --------------------------------------∗
   |={⊤ ∖ ↑N,⊤}=> cinv_own γ p ∗ ▷ P
   
-1 subgoal
+1 goal
   
   Σ : gFunctors
   invG0 : invG Σ
@@ -86,7 +86,7 @@
   |={⊤}=> (▷ <pers> P ∗ na_own t (E2 ∖ ↑N))
           ∗ (na_own t E2 ={⊤}=∗ na_own t E1 ∗ na_own t E2 ∗ ▷ P)
   
-1 subgoal
+1 goal
   
   Σ : gFunctors
   invG0 : invG Σ
@@ -117,7 +117,7 @@ The command has indeed failed with message:
 Tactic failure: iInv: invariant "H2" not found.
 "test_iInv"
      : string
-1 subgoal
+1 goal
   
   Σ : gFunctors
   invG0 : invG Σ
@@ -133,7 +133,7 @@ Tactic failure: iInv: invariant "H2" not found.
   
 "test_iInv_with_close"
      : string
-1 subgoal
+1 goal
   
   Σ : gFunctors
   invG0 : invG Σ
@@ -150,42 +150,42 @@ Tactic failure: iInv: invariant "H2" not found.
   
 "p1"
      : string
-1 subgoal
+1 goal
   
   PROP : bi
   ============================
   forall P (_ : True), bi_entails P P
 "p2"
      : string
-1 subgoal
+1 goal
   
   PROP : bi
   ============================
   forall P, and True (bi_entails P P)
 "p3"
      : string
-1 subgoal
+1 goal
   
   PROP : bi
   ============================
   ex (fun P => bi_entails P P)
 "p4"
      : string
-1 subgoal
+1 goal
   
   PROP : bi
   ============================
   bi_emp_valid (bi_exist (fun x : nat => bi_pure (eq x O)))
 "p5"
      : string
-1 subgoal
+1 goal
   
   PROP : bi
   ============================
   bi_emp_valid (bi_exist (fun _ : nat => bi_pure (forall y : nat, eq y y)))
 "p6"
      : string
-1 subgoal
+1 goal
   
   PROP : bi
   ============================
@@ -198,7 +198,7 @@ Tactic failure: iInv: invariant "H2" not found.
               bi_sep (bi_pure (forall y : nat, eq y y)) (bi_pure (eq z O))))))
 "p7"
      : string
-1 subgoal
+1 goal
   
   PROP : bi
   ============================
@@ -206,14 +206,14 @@ Tactic failure: iInv: invariant "H2" not found.
   bi_entails (bi_pure True) (bi_pure (ge y O))
 "p8"
      : string
-1 subgoal
+1 goal
   
   PROP : bi
   ============================
   forall (a : nat) (_ : eq a O) (y : nat), bi_emp_valid (bi_pure (ge y O))
 "p9"
      : string
-1 subgoal
+1 goal
   
   PROP : bi
   ============================
diff --git a/tests/proofmode_iris.ref b/tests/proofmode_iris.ref
index 6e2f09efef0b374c4a64b174a669897f2fc4d632..dc20ed5696e88438d41e445c85d2448de207cd53 100644
--- a/tests/proofmode_iris.ref
+++ b/tests/proofmode_iris.ref
@@ -1,4 +1,4 @@
-1 subgoal
+1 goal
   
   Σ : gFunctors
   invG0 : invG Σ
@@ -12,7 +12,7 @@
   --------------------------------------â–¡
   |={⊤ ∖ ↑N}=> ▷ <pers> P ∗ (|={⊤}=> ▷ P)
   
-1 subgoal
+1 goal
   
   Σ : gFunctors
   invG0 : invG Σ
@@ -28,7 +28,7 @@
   --------------------------------------∗
   |={⊤ ∖ ↑N,⊤}=> ▷ P
   
-1 subgoal
+1 goal
   
   Σ : gFunctors
   invG0 : invG Σ
@@ -40,7 +40,7 @@
   P : iProp Σ
   ============================
   cinv N γ (<pers> P) ∗ cinv_own γ p ={⊤}=∗ cinv_own γ p ∗ ▷ P
-1 subgoal
+1 goal
   
   Σ : gFunctors
   invG0 : invG Σ
@@ -58,7 +58,7 @@
   --------------------------------------∗
   |={⊤ ∖ ↑N}=> ▷ <pers> P ∗ (|={⊤}=> cinv_own γ p ∗ ▷ P)
   
-1 subgoal
+1 goal
   
   Σ : gFunctors
   invG0 : invG Σ
@@ -77,7 +77,7 @@
   --------------------------------------∗
   |={⊤ ∖ ↑N,⊤}=> cinv_own γ p ∗ ▷ P
   
-1 subgoal
+1 goal
   
   Σ : gFunctors
   invG0 : invG Σ
@@ -98,7 +98,7 @@
   |={⊤}=> (▷ <pers> P ∗ na_own t (E2 ∖ ↑N))
           ∗ (na_own t E2 ={⊤}=∗ na_own t E1 ∗ na_own t E2 ∗ ▷ P)
   
-1 subgoal
+1 goal
   
   Σ : gFunctors
   invG0 : invG Σ
@@ -112,7 +112,7 @@
   ↑N ⊆ E2
   → na_inv t N (<pers> P) ∗ na_own t E1 ∗ na_own t E2
     ={⊤}=∗ na_own t E1 ∗ na_own t E2 ∗ ▷ P
-1 subgoal
+1 goal
   
   Σ : gFunctors
   invG0 : invG Σ
@@ -143,7 +143,7 @@ The command has indeed failed with message:
 Tactic failure: iInv: invariant "H2" not found.
 "test_frac_split_combine"
      : string
-1 subgoal
+1 goal
   
   Σ : gFunctors
   invG0 : invG Σ
@@ -157,7 +157,7 @@ Tactic failure: iInv: invariant "H2" not found.
   --------------------------------------∗
   own γ 1%Qp
   
-1 subgoal
+1 goal
   
   Σ : gFunctors
   invG0 : invG Σ
@@ -172,7 +172,7 @@ Tactic failure: iInv: invariant "H2" not found.
   
 "test_iInv"
      : string
-1 subgoal
+1 goal
   
   Σ : gFunctors
   invG0 : invG Σ
@@ -188,7 +188,7 @@ Tactic failure: iInv: invariant "H2" not found.
   
 "test_iInv_with_close"
      : string
-1 subgoal
+1 goal
   
   Σ : gFunctors
   invG0 : invG Σ
diff --git a/tests/proofmode_monpred.ref b/tests/proofmode_monpred.ref
index bca8ecb7704378c8ed81bf3baaab93364edd37c3..be3c1169d610c66856153aa4fc6a107a03c0e9ac 100644
--- a/tests/proofmode_monpred.ref
+++ b/tests/proofmode_monpred.ref
@@ -1,4 +1,4 @@
-1 subgoal
+1 goal
   
   I : biIndex
   PROP : bi
@@ -9,7 +9,7 @@
   --------------------------------------∗
   (P -∗ Q) i
   
-1 subgoal
+1 goal
   
   I : biIndex
   PROP : bi
@@ -21,7 +21,7 @@
   --------------------------------------∗
   Q j
   
-1 subgoal
+1 goal
   
   I : biIndex
   PROP : bi
@@ -35,7 +35,7 @@
   --------------------------------------∗
   ∀ i, 𝓟 ∗ 𝓠 ∗ Q i
   
-1 subgoal
+1 goal
   
   I : biIndex
   PROP : bi
@@ -46,7 +46,7 @@
   --------------------------------------∗
   (Q -∗ emp) i
   
-1 subgoal
+1 goal
   
   I : biIndex
   PROP : bi
@@ -59,7 +59,7 @@
   
 The command has indeed failed with message:
 Tactic failure: iFrame: cannot frame (P i).
-1 subgoal
+1 goal
   
   I : biIndex
   Σ : gFunctors
@@ -72,7 +72,7 @@ Tactic failure: iFrame: cannot frame (P i).
   --------------------------------------â–¡
   |={⊤ ∖ ↑N}=> ⎡ ▷ <pers> 𝓟 ⎤ ∗ (|={⊤}=> ⎡ ▷ 𝓟 ⎤)
   
-1 subgoal
+1 goal
   
   I : biIndex
   Σ : gFunctors
diff --git a/tests/telescopes.ref b/tests/telescopes.ref
index 78bea449476f8569ef3257c881b734c623946454..2743ec03a2202e03bd0d449c8c306818eae58398 100644
--- a/tests/telescopes.ref
+++ b/tests/telescopes.ref
@@ -1,4 +1,4 @@
-1 subgoal
+1 goal
   
   PROP : bi
   BiFUpd0 : BiFUpd PROP
@@ -13,7 +13,7 @@
   --------------------------------------∗
   |={E2}=> ∃.. x : X, α x ∗ (β x ={E2,E1}=∗ γ2 x)
   
-1 subgoal
+1 goal
   
   PROP : bi
   BiFUpd0 : BiFUpd PROP
@@ -22,7 +22,7 @@
   α, β, γ1, γ2 : X → PROP
   ============================
   accessor E1 E2 α β γ1 -∗ accessor E1 E2 α β (λ.. x : X, γ1 x ∨ γ2 x)
-1 subgoal
+1 goal
   
   PROP : bi
   BiFUpd0 : BiFUpd PROP
@@ -35,7 +35,7 @@
   --------------------------------------∗
   (λ.. x0 : X, γ1 x0 ∨ γ2 x0) x
   
-1 subgoal
+1 goal
   
   PROP : bi
   BiFUpd0 : BiFUpd PROP
@@ -48,7 +48,7 @@
   --------------------------------------∗
   γ1 x ∨ γ2 x
   
-1 subgoal
+1 goal
   
   PROP : bi
   BiFUpd0 : BiFUpd PROP
@@ -60,7 +60,7 @@
   
 "test1_test"
      : string
-1 subgoal
+1 goal
   
   PROP : bi
   x : nat
@@ -69,7 +69,7 @@
   --------------------------------------∗
   â–· False
   
-1 subgoal
+1 goal
   
   PROP : bi
   x : nat
@@ -80,7 +80,7 @@
   
 "test2_test"
      : string
-1 subgoal
+1 goal
   
   PROP : bi
   ============================
@@ -88,7 +88,7 @@
   --------------------------------------∗
   False
   
-1 subgoal
+1 goal
   
   PROP : bi
   x : nat
@@ -97,7 +97,7 @@
   --------------------------------------∗
   False
   
-1 subgoal
+1 goal
   
   PROP : bi
   x : nat
@@ -108,7 +108,7 @@
   
 "test3_test"
      : string
-1 subgoal
+1 goal
   
   PROP : bi
   x : nat
@@ -117,7 +117,7 @@
   --------------------------------------∗
   â–· False
   
-1 subgoal
+1 goal
   
   PROP : bi
   x : nat