33 files changed, 148 insertions, 148 deletions

diff --git a/engine/evd.ml b/engine/evd.ml
index 706e51d4b3..ed40b63d14 100644
--- a/engine/evd.ml
+++ b/engine/evd.ml
@@ -525,7 +525,7 @@ end = struct
       let principal =
         if principal then
           match fgl.principal with
-          | Some _ -> CErrors.user_err Pp.(str "Only one main subgoal per instantiation.")
+          | Some _ -> CErrors.user_err Pp.(str "Only one main goal per instantiation.")
           | None -> Some evk
         else fgl.principal
       in
diff --git a/ide/coqide/wg_ProofView.ml b/ide/coqide/wg_ProofView.ml
index 01dfed0067..fa37edd82b 100644
--- a/ide/coqide/wg_ProofView.ml
+++ b/ide/coqide/wg_ProofView.ml
@@ -66,7 +66,7 @@ let mode_tactic sel_cb (proof : #GText.view_skel) goals ~unfoc_goals hints = mat
       in
       let goals_cnt = List.length rem_goals + 1 in
       let head_str = Printf.sprintf
-        "%d subgoal%s\n" goals_cnt (if 1 < goals_cnt then "s" else "")
+        "%d goal%s\n" goals_cnt (if 1 < goals_cnt then "s" else "")
       in
       let goal_str ?(shownum=false) index total id =
         let annot =
@@ -148,10 +148,10 @@ let display mode (view : #GText.view_skel) goals hints evars =
     let evars = match evars with None -> [] | Some evs -> evs in
     begin match (bg, shelved_goals,given_up_goals, evars) with
     | [], [], [], [] ->
-      view#buffer#insert "No more subgoals."
+      view#buffer#insert "No more goals."
     | [], [], [], _ :: _ ->
       (* A proof has been finished, but not concluded *)
-      view#buffer#insert "No more subgoals, but there are non-instantiated existential variables:\n\n";
+      view#buffer#insert "No more goals, but there are non-instantiated existential variables:\n\n";
       let iter evar =
         let msg = Printf.sprintf "%s\n" evar.Interface.evar_info in
         view#buffer#insert msg
@@ -160,7 +160,7 @@ let display mode (view : #GText.view_skel) goals hints evars =
       view#buffer#insert "\nYou can use Grab Existential Variables."
     | [], [], _, _ ->
       (* The proof is finished, with the exception of given up goals. *)
-      view#buffer#insert "No more subgoals, but there are some goals you gave up:\n\n";
+      view#buffer#insert "No more goals, but there are some goals you gave up:\n\n";
       let iter goal =
         insert_xml view#buffer (Richpp.richpp_of_pp width goal.Interface.goal_ccl);
         view#buffer#insert "\n"
diff --git a/plugins/cc/cctac.ml b/plugins/cc/cctac.ml
index 499c9684b2..72f77508d8 100644
--- a/plugins/cc/cctac.ml
+++ b/plugins/cc/cctac.ml
@@ -420,7 +420,7 @@ let cc_tactic depth additionnal_terms =
   Proofview.Goal.enter begin fun gl ->
     let sigma = Tacmach.New.project gl in
     Coqlib.(check_required_library logic_module_name);
-    let _ = debug (fun () -> Pp.str "Reading subgoal ...") in
+    let _ = debug (fun () -> Pp.str "Reading goal ...") in
     let state = make_prb gl depth additionnal_terms in
     let _ = debug (fun () -> Pp.str "Problem built, solving ...") in
     let sol = execute true state in
diff --git a/plugins/ssr/ssrtacticals.ml b/plugins/ssr/ssrtacticals.ml
index cbc352126e..c822675589 100644
--- a/plugins/ssr/ssrtacticals.ml
+++ b/plugins/ssr/ssrtacticals.ml
@@ -40,7 +40,7 @@ let tclPERM perm tac =
 let rot_hyps dir i hyps =
   let n = List.length hyps in
   if i = 0 then List.rev hyps else
-  if i > n then CErrors.user_err (Pp.str "Not enough subgoals") else
+  if i > n then CErrors.user_err (Pp.str "Not enough goals") else
   let rec rot i l_hyps = function
     | hyp :: hyps' when i > 0 -> rot (i - 1) (hyp :: l_hyps) hyps'
     | hyps' -> hyps' @ (List.rev l_hyps) in
diff --git a/printing/printer.ml b/printing/printer.ml
index 1425cebafc..ca9dee2df6 100644
--- a/printing/printer.ml
+++ b/printing/printer.ml
@@ -480,7 +480,7 @@ let pr_goal_name sigma g =
 
 let pr_goal_header nme sigma g =
   let (g,sigma) = Goal.V82.nf_evar sigma g in
-  str "subgoal " ++ nme ++ (if should_tag() then pr_goal_tag g else str"")
+  str "goal " ++ nme ++ (if should_tag() then pr_goal_tag g else str"")
   ++ (if should_gname() then str " " ++ Pp.surround (pr_existential_key sigma g) else mt ())
 
 (* display the conclusion of a goal *)
@@ -753,10 +753,10 @@ let pr_subgoals ?(pr_first=true) ?(diffs=false) ?os_map
   | [] ->
     let exl = Evd.undefined_map sigma in
     if Evar.Map.is_empty exl then
-      v 0 (str "No more subgoals." ++ pr_evar_info None sigma seeds)
+      v 0 (str "No more goals." ++ pr_evar_info None sigma seeds)
     else
       let pei = pr_evars_int sigma ~shelf ~given_up:[] 1 exl in
-      v 0 ((str "No more subgoals,"
+      v 0 ((str "No more goals,"
           ++ str " but there are non-instantiated existential variables:"
           ++ cut () ++ (hov 0 pei)
           ++ pr_evar_info None sigma seeds
@@ -765,9 +765,9 @@ let pr_subgoals ?(pr_first=true) ?(diffs=false) ?os_map
       let goals = print_multiple_goals g1 rest in
       let ngoals = List.length rest+1 in
       v 0 (
-        int ngoals ++ focused_if_needed ++ str(String.plural ngoals "subgoal")
+        int ngoals ++ focused_if_needed ++ str(String.plural ngoals "goal")
         ++ print_extra
-        ++ str (if pr_first && (should_gname()) && ngoals > 1 then ", subgoal 1" else "")
+        ++ str (if pr_first && (should_gname()) && ngoals > 1 then ", goal 1" else "")
         ++ (if pr_first && should_tag() then pr_goal_tag g1 else str"")
         ++ (if pr_first then pr_goal_name sigma g1 else mt()) ++ cut () ++ goals
         ++ (if unfocused=[] then str ""
@@ -792,7 +792,7 @@ let pr_open_subgoals_diff ?(quiet=false) ?(diffs=false) ?oproof proof =
           begin match bgoals,shelf,given_up with
           | [] , [] , g when Evar.Set.is_empty g -> pr_subgoals None sigma ~seeds ~shelf ~stack ~unfocused:[] ~goals
           | [] , [] , _ ->
-             Feedback.msg_info (str "No more subgoals, but there are some goals you gave up:");
+             Feedback.msg_info (str "No more goals, but there are some goals you gave up:");
              fnl ()
             ++ pr_subgoals ~pr_first:false None bsigma ~seeds ~shelf:[] ~stack:[] ~unfocused:[] ~goals:(Evar.Set.elements given_up)
             ++ fnl () ++ str "You need to go back and solve them."
diff --git a/proofs/proof_bullet.ml b/proofs/proof_bullet.ml
index 41cb7399da..dc5a1b0ac2 100644
--- a/proofs/proof_bullet.ml
+++ b/proofs/proof_bullet.ml
@@ -68,7 +68,7 @@ module Strict = struct
     match sugg with
     | NeedClosingBrace -> Pp.(str"Try unfocusing with \"}\".")
     | NoBulletInUse -> assert false (* This should never raise an error. *)
-    | ProofFinished -> Pp.(str"No more subgoals.")
+    | ProofFinished -> Pp.(str"No more goals.")
     | Suggest b -> Pp.(str"Expecting " ++ pr_bullet b ++ str".")
     | Unfinished b -> Pp.(str"Current bullet " ++ pr_bullet b ++ str" is not finished.")
 
diff --git a/stm/partac.ml b/stm/partac.ml
index 8232b017f9..6143ac450b 100644
--- a/stm/partac.ml
+++ b/stm/partac.ml
@@ -125,7 +125,7 @@ end = struct (* {{{ *)
                       str" existentials remain unsolved: " ++ prlist (Termops.pr_existential_key sigma) (Evar.Set.elements evars))
        )
     with e when CErrors.noncritical e ->
-      RespError (CErrors.print e ++ spc() ++ str "(for subgoal "++int r_goalno ++ str ")")
+      RespError (CErrors.print e ++ spc() ++ str "(for goal "++int r_goalno ++ str ")")
 
   let name_of_task { t_name } = t_name
   let name_of_request { r_name } = r_name
@@ -163,7 +163,7 @@ let enable_par ~nworkers = ComTactic.set_par_implementation
     let open TacTask in
     let results = (Proof.data p).Proof.goals |> CList.map_i (fun i g ->
       let g_solution, t_assign =
-      Future.create_delegate ~name:(Printf.sprintf "subgoal %d" i)
+      Future.create_delegate ~name:(Printf.sprintf "goal %d" i)
           (fun x -> x) in
       TaskQueue.enqueue_task queue
       ~cancel_switch:(ref false)
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
diff --git a/tools/coqdoc/output.ml b/tools/coqdoc/output.ml
index 10edb0b4db..50aa658128 100644
--- a/tools/coqdoc/output.ml
+++ b/tools/coqdoc/output.ml
@@ -48,7 +48,7 @@ let is_keyword =
       "Delimit"; "Bind"; "Open"; "Scope"; "Inline";
       "Implicit Arguments"; "Add"; "Strict";
       "Typeclasses"; "Instance"; "Global Instance"; "Class"; "Instantiation";
-      "subgoal"; "subgoals"; "vm_compute";
+      "goal"; "goals"; "vm_compute";
       "Opaque"; "Transparent"; "Time";
       "Extraction"; "Extract";
       "Variant";