Avoid using "subgoals" in the UI, it means the same as "goals"

25 files changed, 131 insertions, 131 deletions

diff --git a/test-suite/output-coqtop/DependentEvars.out b/test-suite/output-coqtop/DependentEvars.out
index 2e69b94505..11d1ca0bdb 100644
--- a/test-suite/output-coqtop/DependentEvars.out
+++ b/test-suite/output-coqtop/DependentEvars.out
@@ -1,6 +1,6 @@
 
 Coq < 
-Coq < Coq < 1 subgoal
+Coq < Coq < 1 goal
   
   ============================
   forall P Q R : Prop, (Q -> R) -> (P -> Q) -> (P -> Q) -> P -> R
@@ -8,12 +8,12 @@ Coq < Coq < 1 subgoal
 (dependent evars: ; in current goal:)
 
 strange_imp_trans < 
-strange_imp_trans < No more subgoals.
+strange_imp_trans < No more goals.
 
 (dependent evars: ; in current goal:)
 
 strange_imp_trans < 
-Coq < Coq < 1 subgoal
+Coq < Coq < 1 goal
   
   ============================
   forall P Q : Prop, (P -> Q) /\ P -> Q
@@ -21,7 +21,7 @@ Coq < Coq < 1 subgoal
 (dependent evars: ; in current goal:)
 
 modpon < 
-modpon < No more subgoals.
+modpon < No more goals.
 
 (dependent evars: ; in current goal:)
 
@@ -38,7 +38,7 @@ Coq < p123 is declared
 
 Coq < p34 is declared
 
-Coq < Coq < 1 subgoal
+Coq < Coq < 1 goal
   
   P1, P2, P3, P4 : Prop
   p12 : P1 -> P2
@@ -50,7 +50,7 @@ Coq < Coq < 1 subgoal
 (dependent evars: ; in current goal:)
 
 p14 < 
-p14 < 4 focused subgoals
+p14 < 4 focused goals
 (shelved: 2)
   
   P1, P2, P3, P4 : Prop
@@ -60,16 +60,16 @@ p14 < 4 focused subgoals
   ============================
   ?Q -> P4
 
-subgoal 2 is:
+goal 2 is:
  ?P -> ?Q
-subgoal 3 is:
+goal 3 is:
  ?P -> ?Q
-subgoal 4 is:
+goal 4 is:
  ?P
 
 (dependent evars: ?X4:?P, ?X5:?Q; in current goal: ?X5)
 
-p14 < 3 focused subgoals
+p14 < 3 focused goals
 (shelved: 2)
   
   P1, P2, P3, P4 : Prop
@@ -79,9 +79,9 @@ p14 < 3 focused subgoals
   ============================
   ?P -> (?P0 -> P4) /\ ?P0
 
-subgoal 2 is:
+goal 2 is:
  ?P -> (?P0 -> P4) /\ ?P0
-subgoal 3 is:
+goal 3 is:
  ?P
 
 (dependent evars: ?X4:?P, ?X5 using ?X10 ?X11, ?X10 using ?X11, ?X11:?P0; in current goal: ?X4 ?X5 ?X10 ?X11)
diff --git a/test-suite/output-coqtop/DependentEvars2.out b/test-suite/output-coqtop/DependentEvars2.out
index 63bfafa88d..6bf2c35ad4 100644
--- a/test-suite/output-coqtop/DependentEvars2.out
+++ b/test-suite/output-coqtop/DependentEvars2.out
@@ -1,6 +1,6 @@
 
 Coq < 
-Coq < Coq < 1 subgoal
+Coq < Coq < 1 goal
   
   ============================
   forall P Q R : Prop, (Q -> R) -> (P -> Q) -> (P -> Q) -> P -> R
@@ -8,12 +8,12 @@ Coq < Coq < 1 subgoal
 (dependent evars: ; in current goal:)
 
 strange_imp_trans < 
-strange_imp_trans < No more subgoals.
+strange_imp_trans < No more goals.
 
 (dependent evars: ; in current goal:)
 
 strange_imp_trans < 
-Coq < Coq < 1 subgoal
+Coq < Coq < 1 goal
   
   ============================
   forall P Q : Prop, (P -> Q) /\ P -> Q
@@ -21,7 +21,7 @@ Coq < Coq < 1 subgoal
 (dependent evars: ; in current goal:)
 
 modpon < 
-modpon < No more subgoals.
+modpon < No more goals.
 
 (dependent evars: ; in current goal:)
 
@@ -38,7 +38,7 @@ Coq < p123 is declared
 
 Coq < p34 is declared
 
-Coq < Coq < 1 subgoal
+Coq < Coq < 1 goal
   
   P1, P2, P3, P4 : Prop
   p12 : P1 -> P2
@@ -52,7 +52,7 @@ Coq < Coq < 1 subgoal
 p14 < 
 p14 < Second proof:
 
-p14 < 4 focused subgoals
+p14 < 4 focused goals
 (shelved: 2)
   
   P1, P2, P3, P4 : Prop
@@ -62,16 +62,16 @@ p14 < 4 focused subgoals
   ============================
   ?Q -> P4
 
-subgoal 2 is:
+goal 2 is:
  ?P -> ?Q
-subgoal 3 is:
+goal 3 is:
  ?P -> ?Q
-subgoal 4 is:
+goal 4 is:
  ?P
 
 (dependent evars: ?X4:?P, ?X5:?Q; in current goal: ?X5)
 
-p14 < 1 focused subgoal
+p14 < 1 focused goal
 (shelved: 2)
   
   P1, P2, P3, P4 : Prop
@@ -86,19 +86,19 @@ p14 < 1 focused subgoal
 p14 < This subproof is complete, but there are some unfocused goals.
 Try unfocusing with "}".
 
-3 subgoals
+3 goals
 (shelved: 2)
 
-subgoal 1 is:
+goal 1 is:
  ?P -> (?P0 -> P4) /\ ?P0
-subgoal 2 is:
+goal 2 is:
  ?P -> (?P0 -> P4) /\ ?P0
-subgoal 3 is:
+goal 3 is:
  ?P
 
 (dependent evars: ?X4:?P, ?X5 using ?X10 ?X11, ?X10 using ?X11, ?X11:?P0; in current goal:)
 
-p14 < 3 focused subgoals
+p14 < 3 focused goals
 (shelved: 2)
   
   P1, P2, P3, P4 : Prop
@@ -108,9 +108,9 @@ p14 < 3 focused subgoals
   ============================
   ?P -> (?P0 -> P4) /\ ?P0
 
-subgoal 2 is:
+goal 2 is:
  ?P -> (?P0 -> P4) /\ ?P0
-subgoal 3 is:
+goal 3 is:
  ?P
 
 (dependent evars: ?X4:?P, ?X5 using ?X10 ?X11, ?X10 using ?X11, ?X11:?P0; in current goal: ?X4 ?X5 ?X10 ?X11)
diff --git a/test-suite/output-coqtop/ShowGoal.out b/test-suite/output-coqtop/ShowGoal.out
index 42d9ff31e9..467112f153 100644
--- a/test-suite/output-coqtop/ShowGoal.out
+++ b/test-suite/output-coqtop/ShowGoal.out
@@ -1,52 +1,52 @@
 

-Coq < 1 subgoal

+Coq < 1 goal

   

   ============================

   forall i : nat, exists j k : nat, i = j /\ j = k /\ i = k

 

 x < 

-x < 1 focused subgoal

+x < 1 focused goal

 (shelved: 1)

   

   i : nat

   ============================

   exists k : nat, i = ?j /\ ?j = k /\ i = k

 

-x < 1 focused subgoal

+x < 1 focused goal

 (shelved: 2)

   

   i : nat

   ============================

   i = ?j /\ ?j = ?k /\ i = ?k

 

-x < 2 focused subgoals

+x < 2 focused goals

 (shelved: 2)

   

   i : nat

   ============================

   i = ?j

 

-subgoal 2 is:

+goal 2 is:

  ?j = ?k /\ i = ?k

 

-x < 1 focused subgoal

+x < 1 focused goal

 (shelved: 1)

   

   i : nat

   ============================

   i = ?k /\ i = ?k

 

-x < 2 focused subgoals

+x < 2 focused goals

 (shelved: 1)

   

   i : nat

   ============================

   i = ?k

 

-subgoal 2 is:

+goal 2 is:

  i = ?k

 

-x < 1 subgoal

+x < 1 goal

   

   i : nat

   ============================

diff --git a/test-suite/output-coqtop/ShowProofDiffs.out b/test-suite/output-coqtop/ShowProofDiffs.out
index 285a3bcd89..a37e3e5af4 100644
--- a/test-suite/output-coqtop/ShowProofDiffs.out
+++ b/test-suite/output-coqtop/ShowProofDiffs.out
@@ -1,11 +1,11 @@
 

-Coq < Coq < 1 subgoal

+Coq < Coq < 1 goal

   

   ============================

   forall i : nat, exists j k : nat, i = j /\ j = k /\ i = k

 

 x < 

-x < 1 focused subgoal

+x < 1 focused goal

 (shelved: 1)

   i : nat

   ============================

@@ -14,7 +14,7 @@ x < 1 focused subgoal
 (fun i : nat =>

  ex_intro (fun j : nat => exists k : nat, i = j /\ j = k /\ i = k) ?j ?Goal)

 

-x < 1 focused subgoal

+x < 1 focused goal

 (shelved: 2)

   i : nat

   ============================

@@ -24,13 +24,13 @@ x < 1 focused subgoal
  ex_intro (fun j : nat => exists k : nat, i = j /\ j = k /\ i = k) 

    ?j (ex_intro (fun k : nat => i = ?j /\ ?j = k /\ i = k) ?k ?Goal))

 

-x < 2 focused subgoals

+x < 2 focused goals

 (shelved: 2)

   i : nat

   ============================

   i = ?j

 

-subgoal 2 is:

+goal 2 is:

  ?j = ?k /\ i = ?k

 

 (fun i : nat =>

diff --git a/test-suite/output/Cases.out b/test-suite/output/Cases.out
index 6fd4d37ab4..ea647a990a 100644
--- a/test-suite/output/Cases.out
+++ b/test-suite/output/Cases.out
@@ -89,7 +89,7 @@ Arguments lem2 _%bool_scope
 lem3 = 
 fun dd : nat * nat => let (bb, cc) as aa return (aa = aa) := dd in eq_refl
      : forall k : nat * nat, k = k
-1 subgoal
+1 goal
   
   x : nat
   n, n0 := match x + 0 with
@@ -109,7 +109,7 @@ fun dd : nat * nat => let (bb, cc) as aa return (aa = aa) := dd in eq_refl
             end : x = x
   ============================
   x + 0 = 0
-1 subgoal
+1 goal
   
   p : nat
   a,
diff --git a/test-suite/output/CompactContexts.out b/test-suite/output/CompactContexts.out
index 9d1d19877e..f0a8019b67 100644
--- a/test-suite/output/CompactContexts.out
+++ b/test-suite/output/CompactContexts.out
@@ -1,4 +1,4 @@
-1 subgoal
+1 goal
   
   hP1 : True
   a : nat   b : list nat   h : forall x : nat, {y : nat | y > x}
diff --git a/test-suite/output/Intuition.out b/test-suite/output/Intuition.out
index f2bf25ca65..e273307d75 100644
--- a/test-suite/output/Intuition.out
+++ b/test-suite/output/Intuition.out
@@ -1,4 +1,4 @@
-1 subgoal
+1 goal
   
   m, n : Z
   H : (m >= n)%Z
diff --git a/test-suite/output/Naming.out b/test-suite/output/Naming.out
index 0a989646cf..2daa5a6bb5 100644
--- a/test-suite/output/Naming.out
+++ b/test-suite/output/Naming.out
@@ -1,23 +1,23 @@
-1 subgoal
+1 goal
   
   x3 : nat
   ============================
   forall x x1 x4 x0 : nat,
   (forall x2 x5 : nat, x2 + x1 = x4 + x5) -> x + x1 = x4 + x0
-1 subgoal
+1 goal
   
   x3, x, x1, x4, x0 : nat
   H : forall x x3 : nat, x + x1 = x4 + x3
   ============================
   x + x1 = x4 + x0
-1 subgoal
+1 goal
   
   x3 : nat
   ============================
   forall x x1 x4 x0 : nat,
   (forall x2 x5 : nat, x2 + x1 = x4 + x5 -> foo (S x2 + x1)) ->
   x + x1 = x4 + x0 -> foo (S x)
-1 subgoal
+1 goal
   
   x3 : nat
   ============================
@@ -27,7 +27,7 @@
    forall x6 x7 x8 S0 : nat, x6 + S0 = x7 + x8 + (S x2 + x1)) ->
   x + x1 = x4 + x0 ->
   forall x5 x6 x7 S : nat, x5 + S = x6 + x7 + Datatypes.S x
-1 subgoal
+1 goal
   
   x3, x, x1, x4, x0 : nat
   ============================
@@ -36,7 +36,7 @@
    forall x6 x7 x8 S0 : nat, x6 + S0 = x7 + x8 + (S x2 + x1)) ->
   x + x1 = x4 + x0 ->
   forall x5 x6 x7 S : nat, x5 + S = x6 + x7 + Datatypes.S x
-1 subgoal
+1 goal
   
   x3, x, x1, x4, x0 : nat
   H : forall x x3 : nat,
@@ -45,7 +45,7 @@
   H0 : x + x1 = x4 + x0
   ============================
   forall x5 x6 x7 S : nat, x5 + S = x6 + x7 + Datatypes.S x
-1 subgoal
+1 goal
   
   x3, x, x1, x4, x0 : nat
   H : forall x x3 : nat,
@@ -55,7 +55,7 @@
   x5, x6, x7, S : nat
   ============================
   x5 + S = x6 + x7 + Datatypes.S x
-1 subgoal
+1 goal
   
   x3, a : nat
   H : a = 0 -> forall a : nat, a = 0
diff --git a/test-suite/output/Notations3.out b/test-suite/output/Notations3.out
index a9bed49922..60213cab0c 100644
--- a/test-suite/output/Notations3.out
+++ b/test-suite/output/Notations3.out
@@ -238,7 +238,7 @@ Notation "'exists' ! x .. y , p" :=
   (default interpretation)
 Notation "( x , y , .. , z )" := (pair .. (pair x y) .. z) : core_scope
   (default interpretation)
-1 subgoal
+1 goal
   
   ============================
   ##@%
diff --git a/test-suite/output/Partac.out b/test-suite/output/Partac.out
index 889e698fa2..ce5dbdedb4 100644
--- a/test-suite/output/Partac.out
+++ b/test-suite/output/Partac.out
@@ -1,6 +1,6 @@
 The command has indeed failed with message:
 The term "false" has type "bool" while it is expected to have type "nat".
-(for subgoal 1)
+(for goal 1)
 The command has indeed failed with message:
 The term "0" has type "nat" while it is expected to have type "bool".
-(for subgoal 2)
+(for goal 2)
diff --git a/test-suite/output/Show.out b/test-suite/output/Show.out
index f02e442be5..3db00be048 100644
--- a/test-suite/output/Show.out
+++ b/test-suite/output/Show.out
@@ -1,10 +1,10 @@
-3 subgoals (ID 29)
+3 goals (ID 29)
   
   H : 0 = 0
   ============================
   1 = 1
 
-subgoal 2 (ID 33) is:
+goal 2 (ID 33) is:
  1 = S (S m')
-subgoal 3 (ID 20) is:
+goal 3 (ID 20) is:
  S (S n') = S m
diff --git a/test-suite/output/Unicode.out b/test-suite/output/Unicode.out
index a57b3bbad5..abe6c39e8f 100644
--- a/test-suite/output/Unicode.out
+++ b/test-suite/output/Unicode.out
@@ -1,4 +1,4 @@
-1 subgoal
+1 goal
   
   very_very_long_type_name1 : Type
   very_very_long_type_name2 : Type
@@ -8,7 +8,7 @@
   → True
     → ∀ (x : very_very_long_type_name1) (y : very_very_long_type_name2),
         f x y ∧ f x y ∧ f x y ∧ f x y ∧ f x y ∧ f x y
-1 subgoal
+1 goal
   
   very_very_long_type_name1 : Type
   very_very_long_type_name2 : Type
@@ -18,7 +18,7 @@
   → True
     → ∀ (x : very_very_long_type_name2) (y : very_very_long_type_name1) 
         (z : very_very_long_type_name2), f y x ∧ f y z
-1 subgoal
+1 goal
   
   very_very_long_type_name1 : Type
   very_very_long_type_name2 : Type
@@ -29,7 +29,7 @@
     → ∀ (x : very_very_long_type_name2) (y : very_very_long_type_name1) 
         (z : very_very_long_type_name2),
         f y x ∧ f y z ∧ f y x ∧ f y z ∧ f y x ∧ f y z
-1 subgoal
+1 goal
   
   very_very_long_type_name1 : Type
   very_very_long_type_name2 : Type
diff --git a/test-suite/output/bug_9370.out b/test-suite/output/bug_9370.out
index 0ff151c8b4..8d34b7143a 100644
--- a/test-suite/output/bug_9370.out
+++ b/test-suite/output/bug_9370.out
@@ -1,12 +1,12 @@
-1 subgoal
+1 goal
   
   ============================
   1 = 1
-1 subgoal
+1 goal
   
   ============================
   1 = 1
-1 subgoal
+1 goal
   
   ============================
   1 = 1
diff --git a/test-suite/output/bug_9403.out b/test-suite/output/bug_9403.out
index 850760d5ed..cd1030bd2e 100644
--- a/test-suite/output/bug_9403.out
+++ b/test-suite/output/bug_9403.out
@@ -1,4 +1,4 @@
-1 subgoal
+1 goal
   
   X : tele
   α, β, γ1, γ2 : X → Prop
diff --git a/test-suite/output/bug_9569.out b/test-suite/output/bug_9569.out
index 2d474e4933..e49449679f 100644
--- a/test-suite/output/bug_9569.out
+++ b/test-suite/output/bug_9569.out
@@ -1,16 +1,16 @@
-1 subgoal
+1 goal
   
   ============================
   exists I : True, I = Logic.I
-1 subgoal
+1 goal
   
   ============================
   f True False True False (Logic.True /\ Logic.False)
-1 subgoal
+1 goal
   
   ============================
   [I | I = Logic.I; I = Logic.I] = [I | I = Logic.I; I = Logic.I]
-1 subgoal
+1 goal
   
   ============================
   [I & I = Logic.I | I = Logic.I; Logic.I = I]
diff --git a/test-suite/output/clear.out b/test-suite/output/clear.out
index 42e3abf26f..ea01ac50d7 100644
--- a/test-suite/output/clear.out
+++ b/test-suite/output/clear.out
@@ -1,4 +1,4 @@
-1 subgoal
+1 goal
   
   z := 0 : nat
   ============================
diff --git a/test-suite/output/goal_output.out b/test-suite/output/goal_output.out
index 17c1aaa55b..453f6ee615 100644
--- a/test-suite/output/goal_output.out
+++ b/test-suite/output/goal_output.out
@@ -2,79 +2,79 @@ Nat.t = nat
      : Set
 Nat.t = nat
      : Set
-2 subgoals
+2 goals
   
   ============================
   True
 
-subgoal 2 is:
+goal 2 is:
  True
-2 subgoals, subgoal 1 (?Goal)
+2 goals, goal 1 (?Goal)
   
   ============================
   True
 
-subgoal 2 (?Goal0) is:
+goal 2 (?Goal0) is:
  True
-1 subgoal
+1 goal
   
   ============================
   True
-1 subgoal (?Goal0)
+1 goal (?Goal0)
   
   ============================
   True
-1 subgoal (?Goal0)
+1 goal (?Goal0)
   
   ============================
   True
 
 *** Unfocused goals:
 
-subgoal 2 (?Goal1) is:
+goal 2 (?Goal1) is:
  True
-subgoal 3 (?Goal) is:
+goal 3 (?Goal) is:
  True
-1 subgoal
+1 goal
   
   ============================
   True
 
 *** Unfocused goals:
 
-subgoal 2 is:
+goal 2 is:
  True
-subgoal 3 is:
+goal 3 is:
  True
 This subproof is complete, but there are some unfocused goals.
 Focus next goal with bullet -.
 
-2 subgoals
+2 goals
 
-subgoal 1 is:
+goal 1 is:
  True
-subgoal 2 is:
+goal 2 is:
  True
 This subproof is complete, but there are some unfocused goals.
 Focus next goal with bullet -.
 
-2 subgoals
+2 goals
 
-subgoal 1 (?Goal0) is:
+goal 1 (?Goal0) is:
  True
-subgoal 2 (?Goal) is:
+goal 2 (?Goal) is:
  True
 This subproof is complete, but there are some unfocused goals.
 Focus next goal with bullet -.
 
-1 subgoal
+1 goal
 
-subgoal 1 is:
+goal 1 is:
  True
 This subproof is complete, but there are some unfocused goals.
 Focus next goal with bullet -.
 
-1 subgoal
+1 goal
 
-subgoal 1 (?Goal) is:
+goal 1 (?Goal) is:
  True
diff --git a/test-suite/output/ltac.out b/test-suite/output/ltac.out
index efdc94fb1e..ed42429f85 100644
--- a/test-suite/output/ltac.out
+++ b/test-suite/output/ltac.out
@@ -38,7 +38,7 @@ Ltac foo :=
   let w := () in
   let z := 1 in
   pose v
-2 subgoals
+2 goals
   
   n : nat
   ============================
@@ -47,5 +47,5 @@ Ltac foo :=
                              | S n1 => a n1
                              end) n = n
 
-subgoal 2 is:
+goal 2 is:
  forall a : nat, a = 0
diff --git a/test-suite/output/names.out b/test-suite/output/names.out
index 48be63a46a..051bce7701 100644
--- a/test-suite/output/names.out
+++ b/test-suite/output/names.out
@@ -3,7 +3,7 @@ In environment
 y : nat
 The term "a y" has type "{y0 : nat | y = y0}"
 while it is expected to have type "{x : nat | x = y}".
-1 focused subgoal
+1 focused goal
 (shelved: 1)
   
   H : ?n <= 3 -> 3 <= ?n -> ?n = 3
diff --git a/test-suite/output/optimize_heap.out b/test-suite/output/optimize_heap.out
index 94a0b19118..b6ee61a971 100644
--- a/test-suite/output/optimize_heap.out
+++ b/test-suite/output/optimize_heap.out
@@ -1,8 +1,8 @@
-1 subgoal
+1 goal
   
   ============================
   True
-1 subgoal
+1 goal
   
   ============================
   True
diff --git a/test-suite/output/set.out b/test-suite/output/set.out
index 4b72d73eb3..61f3c52656 100644
--- a/test-suite/output/set.out
+++ b/test-suite/output/set.out
@@ -1,16 +1,16 @@
-1 subgoal
+1 goal
   
   y1 := 0 : nat
   x := 0 + 0 : nat
   ============================
   x = x
-1 subgoal
+1 goal
   
   y1, y2 := 0 : nat
   x := y2 + 0 : nat
   ============================
   x = x
-1 subgoal
+1 goal
   
   y1, y2, y3 := 0 : nat
   x := y2 + y3 : nat
diff --git a/test-suite/output/simpl.out b/test-suite/output/simpl.out
index 526e468f5b..fd35c5e339 100644
--- a/test-suite/output/simpl.out
+++ b/test-suite/output/simpl.out
@@ -1,14 +1,14 @@
-1 subgoal
+1 goal
   
   x : nat
   ============================
   x = S x
-1 subgoal
+1 goal
   
   x : nat
   ============================
   0 + x = S x
-1 subgoal
+1 goal
   
   x : nat
   ============================
diff --git a/test-suite/output/subst.out b/test-suite/output/subst.out
index 209b2bc26f..9cc515b7ba 100644
--- a/test-suite/output/subst.out
+++ b/test-suite/output/subst.out
@@ -1,4 +1,4 @@
-1 subgoal
+1 goal
   
   y, z : nat
   Hy : y = 0
@@ -11,7 +11,7 @@
   H4 : z = 4
   ============================
   True
-1 subgoal
+1 goal
   
   x, z : nat
   Hx : x = 0
@@ -24,7 +24,7 @@
   H4 : z = 4
   ============================
   True
-1 subgoal
+1 goal
   
   x, y : nat
   Hx : x = 0
@@ -37,7 +37,7 @@
   H4 : 0 = 4
   ============================
   True
-1 subgoal
+1 goal
   
   H1 : 0 = 1
   HA : True
@@ -47,7 +47,7 @@
   H4 : 0 = 4
   ============================
   True
-1 subgoal
+1 goal
   
   y, z : nat
   Hy : y = 0
@@ -60,7 +60,7 @@
   H2 : 0 = 2
   ============================
   True
-1 subgoal
+1 goal
   
   x, z : nat
   Hx : x = 0
@@ -73,7 +73,7 @@
   H3 : 0 = 3
   ============================
   True
-1 subgoal
+1 goal
   
   x, y : nat
   Hx : x = 0
@@ -86,7 +86,7 @@
   H4 : 0 = 4
   ============================
   True
-1 subgoal
+1 goal
   
   HA, HB : True
   H4 : 0 = 4
diff --git a/test-suite/output/unifconstraints.out b/test-suite/output/unifconstraints.out
index 2fadd747b7..abcb8d7e0c 100644
--- a/test-suite/output/unifconstraints.out
+++ b/test-suite/output/unifconstraints.out
@@ -1,44 +1,44 @@
-3 focused subgoals
+3 focused goals
 (shelved: 1)
   
   ============================
   ?Goal 0
 
-subgoal 2 is:
+goal 2 is:
  forall n : nat, ?Goal n -> ?Goal (S n)
-subgoal 3 is:
+goal 3 is:
  nat
 unification constraint:
  ?Goal ?Goal2 <=
    True /\ True /\ True \/
    veeryyyyyyyyyyyyloooooooooooooonggidentifier =
    veeryyyyyyyyyyyyloooooooooooooonggidentifier
-3 focused subgoals
+3 focused goals
 (shelved: 1)
   
   n, m : nat
   ============================
   ?Goal@{n:=n; m:=m} 0
 
-subgoal 2 is:
+goal 2 is:
  forall n0 : nat, ?Goal@{n:=n; m:=m} n0 -> ?Goal@{n:=n; m:=m} (S n0)
-subgoal 3 is:
+goal 3 is:
  nat
 unification constraint:
  ?Goal@{n:=n; m:=m} ?Goal2@{n:=n; m:=m} <=
    True /\ True /\ True \/
    veeryyyyyyyyyyyyloooooooooooooonggidentifier =
    veeryyyyyyyyyyyyloooooooooooooonggidentifier
-3 focused subgoals
+3 focused goals
 (shelved: 1)
   
   m : nat
   ============================
   ?Goal1@{m:=m} 0
 
-subgoal 2 is:
+goal 2 is:
  forall n0 : nat, ?Goal1@{m:=m} n0 -> ?Goal1@{m:=m} (S n0)
-subgoal 3 is:
+goal 3 is:
  nat
 unification constraint:
  
@@ -46,16 +46,16 @@ unification constraint:
    True /\ True /\ True \/
    veeryyyyyyyyyyyyloooooooooooooonggidentifier =
    veeryyyyyyyyyyyyloooooooooooooonggidentifier
-3 focused subgoals
+3 focused goals
 (shelved: 1)
   
   m : nat
   ============================
   ?Goal0@{m:=m} 0
 
-subgoal 2 is:
+goal 2 is:
  forall n0 : nat, ?Goal0@{m:=m} n0 -> ?Goal0@{m:=m} (S n0)
-subgoal 3 is:
+goal 3 is:
  nat
 unification constraint:
  
diff --git a/test-suite/output/unification.out b/test-suite/output/unification.out
index cf31871e5a..4db5c2d161 100644
--- a/test-suite/output/unification.out
+++ b/test-suite/output/unification.out
@@ -9,25 +9,25 @@ Unable to unify "T" with "?X@{x0:=x; x:=C a}" (cannot instantiate
 The command has indeed failed with message:
 The term "id" has type "ID" while it is expected to have type 
 "Type -> ?T" (cannot instantiate "?T" because "A" is not in its scope).
-1 focused subgoal
+1 focused goal
 (shelved: 1)
   
   H : forall x : nat, S (S (S x)) = x
   ============================
   ?x = 0
-1 focused subgoal
+1 focused goal
 (shelved: 1)
   
   H : forall x : nat, S (S (S x)) = x
   ============================
   ?x = 0
-1 focused subgoal
+1 focused goal
 (shelved: 1)
   
   H : forall x : nat, S (S (S x)) = x
   ============================
   ?x = 0
-1 focused subgoal
+1 focused goal
 (shelved: 1)
   
   H : forall x : nat, S x = x