50 files changed, 306 insertions, 264 deletions

diff --git a/doc/sphinx/addendum/generalized-rewriting.rst b/doc/sphinx/addendum/generalized-rewriting.rst
index c54db36691..9ac05fab2e 100644
--- a/doc/sphinx/addendum/generalized-rewriting.rst
+++ b/doc/sphinx/addendum/generalized-rewriting.rst
@@ -726,6 +726,30 @@ declare your constant as rigid for proof search using the command
 Strategies for rewriting
 ------------------------
 
+Usage
+~~~~~
+
+.. tacn:: rewrite_strat @rewstrategy {? in @ident }
+   :name: rewrite_strat
+
+   Rewrite using :n:`@rewstrategy` in the conclusion or in the hypothesis :n:`@ident`.
+
+   .. exn:: Nothing to rewrite.
+
+      The strategy didn't find any matches.
+
+   .. exn:: No progress made.
+
+      If the strategy succeeded but made no progress.
+
+   .. exn:: Unable to satisfy the rewriting constraints.
+
+      If the strategy succeeded and made progress but the
+      corresponding rewriting constraints are not satisfied.
+
+   :tacn:`setoid_rewrite` :n:`@one_term` is basically equivalent to
+   :n:`rewrite_strat outermost @one_term`.
+
 Definitions
 ~~~~~~~~~~~
 
@@ -773,7 +797,7 @@ are applied using the tactic :n:`rewrite_strat @rewstrategy`.
    failure
 
 :n:`id`
-  identity
+   identity
 
 :n:`refl`
    reflexivity
@@ -803,10 +827,16 @@ are applied using the tactic :n:`rewrite_strat @rewstrategy`.
    all subterms
 
 :n:`innermost @rewstrategy`
-   innermost first
+   Innermost first.
+   When there are multiple nested matches in a subterm, the innermost subterm
+   is rewritten.  For :ref:`example <rewrite_strat_innermost_outermost>`,
+   rewriting :n:`(a + b) + c` with Nat.add_comm gives :n:`(b + a) + c`.
 
 :n:`outermost @rewstrategy`
-   outermost first
+   Outermost first.
+   When there are multiple nested matches in a subterm, the outermost subterm
+   is rewritten.  For :ref:`example <rewrite_strat_innermost_outermost>`,
+   rewriting :n:`(a + b) + c` with Nat.add_comm gives :n:`c + (a + b)`.
 
 :n:`bottomup @rewstrategy`
    bottom-up
@@ -833,8 +863,8 @@ are applied using the tactic :n:`rewrite_strat @rewstrategy`.
    to be documented
 
 
-A few of these are defined in terms of the others using a
-primitive fixpoint operator:
+Conceptually, a few of these are defined in terms of the others using a
+primitive fixpoint operator `fix`, which the tactic doesn't currently support:
 
 - :n:`try @rewstrategy := choice @rewstrategy id`
 - :n:`any @rewstrategy := fix @ident. try (@rewstrategy ; @ident)`
@@ -876,30 +906,30 @@ if it reduces the subterm under consideration. The ``fold`` strategy takes
 a :token:`term` and tries to *unify* it to the current subterm, converting it to :token:`term`
 on success. It is stronger than the tactic ``fold``.
 
+.. _rewrite_strat_innermost_outermost:
 
-Usage
-~~~~~
-
-
-.. tacn:: rewrite_strat @rewstrategy {? in @ident }
-   :name: rewrite_strat
+.. example:: :n:`innermost` and :n:`outermost`
 
-   Rewrite using the strategy s in hypothesis ident or the conclusion.
+   The type of `Nat.add_comm` is `forall n m : nat, n + m = m + n`.
 
-   .. exn:: Nothing to rewrite.
+   .. coqtop:: all
 
-      If the strategy failed.
+      Require Import Coq.Arith.Arith.
+      Set Printing Parentheses.
+      Goal forall a b c: nat, a + b + c = 0.
+      rewrite_strat innermost Nat.add_comm.
 
-   .. exn:: No progress made.
+   .. coqtop:: none
 
-      If the strategy succeeded but made no progress.
+      Abort.
+      Goal forall a b c: nat, a + b + c = 0.
 
-   .. exn:: Unable to satisfy the rewriting constraints.
+   Using :n:`outermost` instead gives this result:
 
-      If the strategy succeeded and made progress but the
-      corresponding rewriting constraints are not satisfied.
+   .. coqtop:: all
 
+      rewrite_strat outermost Nat.add_comm.
 
-   The ``setoid_rewrite c`` tactic is basically equivalent to
-   ``rewrite_strat (outermost c)``.
+   .. coqtop:: none
 
+      Abort.
diff --git a/doc/sphinx/proof-engine/ltac2.rst b/doc/sphinx/proof-engine/ltac2.rst
index 3646a32a79..1bb4216e4f 100644
--- a/doc/sphinx/proof-engine/ltac2.rst
+++ b/doc/sphinx/proof-engine/ltac2.rst
@@ -554,7 +554,7 @@ Built-in quotations
    ltac2_quotations ::= ident : ( @lident )
    | constr : ( @term )
    | open_constr : ( @term )
-   | pattern : ( @cpattern )
+   | pat : ( @cpattern )
    | reference : ( {| & @ident | @qualid } )
    | ltac1 : ( @ltac1_expr_in_env )
    | ltac1val : ( @ltac1_expr_in_env )
@@ -568,7 +568,7 @@ The current implementation recognizes the following built-in quotations:
   (type ``Init.constr``).
 - ``open_constr``, which parses Coq terms and produces a term potentially with
   holes at runtime (type ``Init.constr`` as well).
-- ``pattern``, which parses Coq patterns and produces a pattern used for term
+- ``pat``, which parses Coq patterns and produces a pattern used for term
   matching (type ``Init.pattern``).
 - ``reference``  Qualified names
   are globalized at internalization into the corresponding global reference,
diff --git a/doc/tools/docgram/common.edit_mlg b/doc/tools/docgram/common.edit_mlg
index 44bb767011..8aeb2e564d 100644
--- a/doc/tools/docgram/common.edit_mlg
+++ b/doc/tools/docgram/common.edit_mlg
@@ -2066,7 +2066,7 @@ ltac2_tactic_atom: [
 | MOVETO ltac2_quotations "constr" ":" "(" lconstr ")"      (* Ltac2 plugin *)
 | MOVETO ltac2_quotations "open_constr" ":" "(" lconstr ")"      (* Ltac2 plugin *)
 | MOVETO ltac2_quotations "ident" ":" "(" lident ")"      (* Ltac2 plugin *)
-| MOVETO ltac2_quotations "pattern" ":" "(" cpattern ")"      (* Ltac2 plugin *)
+| MOVETO ltac2_quotations "pat" ":" "(" cpattern ")"      (* Ltac2 plugin *)
 | MOVETO ltac2_quotations "reference" ":" "(" globref ")"      (* Ltac2 plugin *)
 | MOVETO ltac2_quotations "ltac1" ":" "(" ltac1_expr_in_env ")"      (* Ltac2 plugin *)
 | MOVETO ltac2_quotations "ltac1val" ":" "(" ltac1_expr_in_env ")"      (* Ltac2 plugin *)
diff --git a/doc/tools/docgram/fullGrammar b/doc/tools/docgram/fullGrammar
index 9f2559ffbc..ec23ffe83e 100644
--- a/doc/tools/docgram/fullGrammar
+++ b/doc/tools/docgram/fullGrammar
@@ -3370,7 +3370,7 @@ G_LTAC2_tactic_atom: [
 | "constr" ":" "(" Constr.lconstr ")"      (* Ltac2 plugin *)
 | "open_constr" ":" "(" Constr.lconstr ")"      (* Ltac2 plugin *)
 | "ident" ":" "(" lident ")"      (* Ltac2 plugin *)
-| "pattern" ":" "(" Constr.cpattern ")"      (* Ltac2 plugin *)
+| "pat" ":" "(" Constr.cpattern ")"      (* Ltac2 plugin *)
 | "reference" ":" "(" globref ")"      (* Ltac2 plugin *)
 | "ltac1" ":" "(" ltac1_expr_in_env ")"      (* Ltac2 plugin *)
 | "ltac1val" ":" "(" ltac1_expr_in_env ")"      (* Ltac2 plugin *)
diff --git a/doc/tools/docgram/orderedGrammar b/doc/tools/docgram/orderedGrammar
index b53af609ec..75b32a5800 100644
--- a/doc/tools/docgram/orderedGrammar
+++ b/doc/tools/docgram/orderedGrammar
@@ -2378,7 +2378,7 @@ ltac2_quotations: [
 | "ident" ":" "(" lident ")"
 | "constr" ":" "(" term ")"
 | "open_constr" ":" "(" term ")"
-| "pattern" ":" "(" cpattern ")"
+| "pat" ":" "(" cpattern ")"
 | "reference" ":" "(" [ "&" ident | qualid ] ")"
 | "ltac1" ":" "(" ltac1_expr_in_env ")"
 | "ltac1val" ":" "(" ltac1_expr_in_env ")"
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/interp/constrextern.ml b/interp/constrextern.ml
index f3ba884856..8138b4c6d9 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -1463,23 +1463,33 @@ let rec glob_of_pat avoid env sigma pat = DAst.make @@ match pat with
   | PIf (c,b1,b2) ->
       GIf (glob_of_pat avoid env sigma c, (Anonymous,None),
            glob_of_pat avoid env sigma b1, glob_of_pat avoid env sigma b2)
-  | PCase ({cip_style=Constr.LetStyle; cip_ind_tags=None},PMeta None,tm,[(0,n,b)]) ->
-      let nal,b = it_destRLambda_or_LetIn_names n (glob_of_pat avoid env sigma b) in
+  | PCase ({cip_style=Constr.LetStyle},None,tm,[(0,n,b)]) ->
+      let n, b = glob_of_pat_under_context avoid env sigma (n, b) in
+      let nal = Array.to_list n in
       GLetTuple (nal,(Anonymous,None),glob_of_pat avoid env sigma tm,b)
   | PCase (info,p,tm,bl) ->
       let mat = match bl, info.cip_ind with
         | [], _ -> []
         | _, Some ind ->
-          let bl' = List.map (fun (i,n,c) -> (i,n,glob_of_pat avoid env sigma c)) bl in
-          simple_cases_matrix_of_branches ind bl'
+          let map (i, n, c) =
+            let n, c = glob_of_pat_under_context avoid env sigma (n, c) in
+            let nal = Array.to_list n in
+            let mkPatVar na = DAst.make @@ PatVar na in
+            let p = DAst.make @@ PatCstr ((ind,i+1),List.map mkPatVar nal,Anonymous) in
+            let ids = List.map_filter Nameops.Name.to_option nal in
+            CAst.make @@ (ids,[p],c)
+          in
+          List.map map bl
         | _, None -> anomaly (Pp.str "PCase with some branches but unknown inductive.")
       in
       let mat = if info.cip_extensible then mat @ [any_any_branch] else mat
       in
-      let indnames,rtn = match p, info.cip_ind, info.cip_ind_tags with
-        | PMeta None, _, _ -> (Anonymous,None),None
-        | _, Some ind, Some nargs ->
-          return_type_of_predicate ind nargs (glob_of_pat avoid env sigma p)
+      let indnames,rtn = match p, info.cip_ind with
+        | None, _ -> (Anonymous,None),None
+        | Some p, Some ind ->
+          let nas, p = glob_of_pat_under_context avoid env sigma p in
+          let nas = Array.rev_to_list nas in
+          ((List.hd nas, Some (CAst.make (ind, List.tl nas))), Some p)
         | _ -> anomaly (Pp.str "PCase with non-trivial predicate but unknown inductive.")
       in
       GCases (Constr.RegularStyle,rtn,[glob_of_pat avoid env sigma tm,indnames],mat)
@@ -1523,6 +1533,18 @@ let rec glob_of_pat avoid env sigma pat = DAst.make @@ match pat with
     let glob_of = glob_of_pat avoid env sigma in
     GArray (None, Array.map glob_of t, glob_of def, glob_of ty)
 
+and glob_of_pat_under_context avoid env sigma (nas, pat) =
+  let fold (avoid, env, nas, epat) na =
+    let na, avoid = compute_displayed_name_in_pattern sigma avoid na epat in
+    let env = Termops.add_name na env in
+    let epat = match epat with PLambda (_, _, p) -> p | _ -> assert false in
+    (avoid, env, na :: nas, epat)
+  in
+  let epat = Array.fold_right (fun na p -> PLambda (na, PMeta None, p)) nas pat in
+  let (avoid', env', nas, _) = Array.fold_left fold (avoid, env, [], epat) nas in
+  let pat = glob_of_pat avoid' env' sigma pat in
+  (Array.rev_of_list nas, pat)
+
 let extern_constr_pattern env sigma pat =
   extern true (InConstrEntrySomeLevel,(None,[]))
     (* XXX no vars? *)
diff --git a/kernel/cClosure.ml b/kernel/cClosure.ml
index a32c8f1cd1..8edf916a7a 100644
--- a/kernel/cClosure.ml
+++ b/kernel/cClosure.ml
@@ -1171,16 +1171,6 @@ module FNativeEntries =
         fNInf := { mark = mark Cstr KnownR; term = FConstruct (Univ.in_punivs cNInf) };
         fNaN := { mark = mark Cstr KnownR; term = FConstruct (Univ.in_punivs cNaN) };
       | None -> defined_f_class := false
-    let defined_refl = ref false
-
-    let frefl = ref dummy
-
-    let init_refl retro =
-      match retro.Retroknowledge.retro_refl with
-      | Some crefl ->
-        defined_refl := true;
-        frefl := { mark = mark Cstr KnownR; term = FConstruct (Univ.in_punivs crefl) }
-      | None -> defined_refl := false
 
     let defined_array = ref false
 
@@ -1197,7 +1187,6 @@ module FNativeEntries =
       init_cmp !current_retro;
       init_f_cmp !current_retro;
       init_f_class !current_retro;
-      init_refl !current_retro;
       init_array !current_retro
 
     let check_env env =
diff --git a/kernel/retroknowledge.ml b/kernel/retroknowledge.ml
index f7c4b62d1f..505f6c648d 100644
--- a/kernel/retroknowledge.ml
+++ b/kernel/retroknowledge.ml
@@ -35,7 +35,6 @@ type retroknowledge = {
                     (* PNormal, NNormal, PSubn, NSubn,
                        PZero, NZero, PInf, NInf,
                        NaN *)
-    retro_refl : constructor option
 }
 
 let empty = {
@@ -48,7 +47,6 @@ let empty = {
     retro_cmp = None;
     retro_f_cmp = None;
     retro_f_class = None;
-    retro_refl = None;
 }
 
 type action =
diff --git a/kernel/retroknowledge.mli b/kernel/retroknowledge.mli
index fd412cdd0a..80c0baaf95 100644
--- a/kernel/retroknowledge.mli
+++ b/kernel/retroknowledge.mli
@@ -29,7 +29,6 @@ type retroknowledge = {
                     (* PNormal, NNormal, PSubn, NSubn,
                        PZero, NZero, PInf, NInf,
                        NaN *)
-    retro_refl : constructor option
 }
 
 val empty : retroknowledge
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/pretyping/constr_matching.ml b/pretyping/constr_matching.ml
index c77feeafbb..15d1ddb4ec 100644
--- a/pretyping/constr_matching.ml
+++ b/pretyping/constr_matching.ml
@@ -352,10 +352,9 @@ let matches_core env sigma allow_bound_rels
             (add_binders na1 na2 binding_vars (sorec ctx env subst c1 c2)) d1 d2
 
       | PIf (a1,b1,b1'), Case (ci, u2, pms2, p2, iv, a2, ([|b2;b2'|] as br2)) ->
-          let (ci2, p2, _, a2, br2) = EConstr.expand_case env sigma (ci, u2, pms2, p2, iv, a2, br2) in
-          let b2, b2' = match br2 with [|b2; b2'|] -> b2, b2' | _ -> assert false in
-          let ctx_b2,b2 = decompose_lam_n_decls sigma ci.ci_cstr_ndecls.(0) b2 in
-          let ctx_b2',b2' = decompose_lam_n_decls sigma ci.ci_cstr_ndecls.(1) b2' in
+          let (_, _, _, p2, _, _, br2) = EConstr.annotate_case env sigma (ci, u2, pms2, p2, iv, a2, br2) in
+          let ctx_b2,b2 = br2.(0) in
+          let ctx_b2',b2' = br2.(1) in
           let n = Context.Rel.length ctx_b2 in
           let n' = Context.Rel.length ctx_b2' in
           if Vars.noccur_between sigma 1 n b2 && Vars.noccur_between sigma 1 n' b2' then
@@ -370,7 +369,7 @@ let matches_core env sigma allow_bound_rels
             raise PatternMatchingFailure
 
       | PCase (ci1, p1, a1, br1), Case (ci2, u2, pms2, p2, iv, a2, br2) ->
-          let (ci2, p2, _, a2, br2) = EConstr.expand_case env sigma (ci2, u2, pms2, p2, iv, a2, br2) in
+          let (_, _, _, p2, _, _, br2) = EConstr.annotate_case env sigma (ci2, u2, pms2, p2, iv, a2, br2) in
           let n2 = Array.length br2 in
           let () = match ci1.cip_ind with
           | None -> ()
@@ -383,14 +382,37 @@ let matches_core env sigma allow_bound_rels
             if not ci1.cip_extensible && not (Int.equal (List.length br1) n2)
             then raise PatternMatchingFailure
           in
+          let sorec_under_ctx subst (n, c1) (decls, c2) =
+            let env = push_rel_context decls env in
+            let rec fold (ctx, subst) nas decls = match nas, decls with
+            | [], _ ->
+              (* Historical corner case: less bound variables are allowed in
+                destructuring let-bindings. See #13735. *)
+                (ctx, subst)
+            | na1 :: nas, d :: decls ->
+              let na2 = Context.Rel.Declaration.get_annot d in
+              let t = Context.Rel.Declaration.get_type d in
+              let ctx = push_binder na1 na2 t ctx in
+              let subst = add_binders na1 na2 binding_vars subst in
+              fold (ctx, subst) nas decls
+            | _, [] ->
+              assert false
+            in
+            let ctx, subst = fold (ctx, subst) (Array.to_list n) (List.rev decls) in
+            sorec ctx env subst c1 c2
+          in
           let chk_branch subst (j,n,c) =
             (* (ind,j+1) is normally known to be a correct constructor
                and br2 a correct match over the same inductive *)
             assert (j < n2);
-            sorec ctx env subst c br2.(j)
+            sorec_under_ctx subst (n, c) br2.(j)
+          in
+          let subst = sorec ctx env subst a1 a2 in
+          let subst = match p1 with
+          | None -> subst
+          | Some p1 -> sorec_under_ctx subst p1 p2
           in
-          let chk_head = sorec ctx env (sorec ctx env subst a1 a2) p1 p2 in
-          List.fold_left chk_branch chk_head br1
+          List.fold_left chk_branch subst br1
 
       |	PFix ((ln1,i1),(lna1,tl1,bl1)), Fix ((ln2,i2),(lna2,tl2,bl2))
            when Array.equal Int.equal ln1 ln2 && i1 = i2 ->
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index bb5125f5ed..722a0a2048 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -1160,18 +1160,3 @@ let rec subst_glob_constr env subst = DAst.map (function
           GArray(u,t',def',ty')
 
   )
-
-(* Utilities to transform kernel cases to simple pattern-matching problem *)
-
-let simple_cases_matrix_of_branches ind brs =
-  List.map (fun (i,n,b) ->
-      let nal,c = it_destRLambda_or_LetIn_names n b in
-      let mkPatVar na = DAst.make @@ PatVar na in
-      let p = DAst.make @@ PatCstr ((ind,i+1),List.map mkPatVar nal,Anonymous) in
-      let ids = List.map_filter Nameops.Name.to_option nal in
-      CAst.make @@ (ids,[p],c))
-    brs
-
-let return_type_of_predicate ind nrealargs_tags pred =
-  let nal,p = it_destRLambda_or_LetIn_names (nrealargs_tags@[false]) pred in
-  (List.hd nal, Some (CAst.make (ind, List.tl nal))), Some p
diff --git a/pretyping/detyping.mli b/pretyping/detyping.mli
index 254f772ff8..6d6f7fa97b 100644
--- a/pretyping/detyping.mli
+++ b/pretyping/detyping.mli
@@ -72,14 +72,6 @@ val lookup_index_as_renamed : env -> evar_map -> constr -> int -> int option
 val force_wildcard : unit -> bool
 val synthetize_type : unit -> bool
 
-(** Utilities to transform kernel cases to simple pattern-matching problem *)
-
-val it_destRLambda_or_LetIn_names : bool list -> glob_constr -> Name.t list * glob_constr
-val simple_cases_matrix_of_branches :
-  inductive -> (int * bool list * glob_constr) list -> cases_clauses
-val return_type_of_predicate :
-  inductive -> bool list -> glob_constr -> predicate_pattern * glob_constr option
-
 val subst_genarg_hook :
   (substitution -> Genarg.glob_generic_argument -> Genarg.glob_generic_argument) Hook.t
 
diff --git a/pretyping/pattern.ml b/pretyping/pattern.ml
index f6d61f4892..553511f1bf 100644
--- a/pretyping/pattern.ml
+++ b/pretyping/pattern.ml
@@ -18,7 +18,6 @@ type patvar = Id.t
 type case_info_pattern =
     { cip_style : Constr.case_style;
       cip_ind : inductive option;
-      cip_ind_tags : bool list option; (** indicates LetIn/Lambda in arity *)
       cip_extensible : bool (** does this match end with _ => _ ? *) }
 
 type constr_pattern =
@@ -35,8 +34,8 @@ type constr_pattern =
   | PSort of Sorts.family
   | PMeta of patvar option
   | PIf of constr_pattern * constr_pattern * constr_pattern
-  | PCase of case_info_pattern * constr_pattern * constr_pattern *
-      (int * bool list * constr_pattern) list (** index of constructor, nb of args *)
+  | PCase of case_info_pattern * (Name.t array * constr_pattern) option * constr_pattern *
+      (int * Name.t array * constr_pattern) list (** index of constructor, nb of args *)
   | PFix of (int array * int) * (Name.t array * constr_pattern array * constr_pattern array)
   | PCoFix of int * (Name.t array * constr_pattern array * constr_pattern array)
   | PInt of Uint63.t
diff --git a/pretyping/patternops.ml b/pretyping/patternops.ml
index 47097a0e32..0c4bbf71e2 100644
--- a/pretyping/patternops.ml
+++ b/pretyping/patternops.ml
@@ -24,7 +24,6 @@ open Environ
 let case_info_pattern_eq i1 i2 =
   i1.cip_style == i2.cip_style &&
   Option.equal Ind.CanOrd.equal i1.cip_ind i2.cip_ind &&
-  Option.equal (List.equal (==)) i1.cip_ind_tags i2.cip_ind_tags &&
   i1.cip_extensible == i2.cip_extensible
 
 let rec constr_pattern_eq p1 p2 = match p1, p2 with
@@ -51,7 +50,7 @@ let rec constr_pattern_eq p1 p2 = match p1, p2 with
   constr_pattern_eq t1 t2 && constr_pattern_eq l1 l2 && constr_pattern_eq r1 r2
 | PCase (info1, p1, r1, l1), PCase (info2, p2, r2, l2) ->
   case_info_pattern_eq info1 info2 &&
-  constr_pattern_eq p1 p2 &&
+  Option.equal (fun (nas1, p1) (nas2, p2) -> Array.equal Name.equal nas1 nas2 && constr_pattern_eq p1 p2) p1 p2 &&
   constr_pattern_eq r1 r2 &&
   List.equal pattern_eq l1 l2
 | PFix ((ln1,i1),f1), PFix ((ln2,i2),f2) ->
@@ -74,7 +73,7 @@ let rec constr_pattern_eq p1 p2 = match p1, p2 with
 (** FIXME: fixpoint and cofixpoint should be relativized to pattern *)
 
 and pattern_eq (i1, j1, p1) (i2, j2, p2) =
-  Int.equal i1 i2 && List.equal (==) j1 j2 && constr_pattern_eq p1 p2
+  Int.equal i1 i2 && Array.equal Name.equal j1 j2 && constr_pattern_eq p1 p2
 
 and rec_declaration_eq (n1, c1, r1) (n2, c2, r2) =
   Array.equal Name.equal n1 n2 &&
@@ -92,8 +91,8 @@ let rec occur_meta_pattern = function
   | PIf (c,c1,c2)  ->
       (occur_meta_pattern c) ||
       (occur_meta_pattern c1) || (occur_meta_pattern c2)
-  | PCase(_,p,c,br) ->
-      (occur_meta_pattern p) ||
+  | PCase(_, p,c,br) ->
+      Option.cata (fun (_, p) -> occur_meta_pattern p) false p ||
       (occur_meta_pattern c) ||
       (List.exists (fun (_,_,p) -> occur_meta_pattern p) br)
   | PArray (t,def,ty) ->
@@ -115,10 +114,10 @@ let rec occurn_pattern n = function
   | PIf (c,c1,c2)  ->
       (occurn_pattern n c) ||
       (occurn_pattern n c1) || (occurn_pattern n c2)
-  | PCase(_,p,c,br) ->
-      (occurn_pattern n p) ||
+  | PCase(_, p, c, br) ->
+      Option.cata (fun (nas, p) -> occurn_pattern (Array.length nas + n) p) false p ||
       (occurn_pattern n c) ||
-      (List.exists (fun (_,_,p) -> occurn_pattern n p) br)
+      (List.exists (fun (_, nas, p) -> occurn_pattern (Array.length nas + n) p) br)
   | PMeta _ | PSoApp _ -> true
   | PEvar (_,args) -> List.exists (occurn_pattern n) args
   | PVar _ | PRef _ | PSort _ | PInt _ | PFloat _ -> false
@@ -202,18 +201,25 @@ let pattern_of_constr env sigma t =
       | Evar_kinds.MatchingVar (Evar_kinds.SecondOrderPatVar ido) -> assert false
       | _ ->
         PMeta None)
-    | Case (ci, u, pms, p, iv, a, br) ->
-        let (ci, p, iv, a, br) = Inductive.expand_case env (ci, u, pms, p, iv, a, br) in
+    | Case (ci, u, pms, p0, iv, a, br0) ->
+        let (ci, p, iv, a, br) = Inductive.expand_case env (ci, u, pms, p0, iv, a, br0) in
+        let pattern_of_ctx c (nas, c0) =
+          let ctx, c = Term.decompose_lam_n_decls (Array.length nas) c in
+          let env = push_rel_context ctx env in
+          let c = pattern_of_constr env c in
+          (Array.map Context.binder_name nas, c)
+        in
+        let p = pattern_of_ctx p p0 in
         let cip =
           { cip_style = ci.ci_pp_info.style;
             cip_ind = Some ci.ci_ind;
-            cip_ind_tags = Some ci.ci_pp_info.ind_tags;
             cip_extensible = false }
         in
         let branch_of_constr i c =
-          (i, ci.ci_pp_info.cstr_tags.(i), pattern_of_constr env c)
+          let nas, c = pattern_of_ctx c br0.(i) in
+          (i, nas, c)
         in
-        PCase (cip, pattern_of_constr env p, pattern_of_constr env a,
+        PCase (cip, Some p, pattern_of_constr env a,
                 Array.to_list (Array.mapi branch_of_constr br))
     | Fix (lni,(lna,tl,bl)) ->
        let push env na2 c2 = push_rel (LocalAssum (na2,c2)) env in
@@ -242,7 +248,10 @@ let map_pattern_with_binders g f l = function
   | PLetIn (n,a,t,b) -> PLetIn (n,f l a,Option.map (f l) t,f (g n l) b)
   | PIf (c,b1,b2) -> PIf (f l c,f l b1,f l b2)
   | PCase (ci,po,p,pl) ->
-    PCase (ci,f l po,f l p, List.map (fun (i,n,c) -> (i,n,f l c)) pl)
+    let fold nas l = Array.fold_left (fun l na -> g na l) l nas in
+    let map_branch (i, n, c) = (i, n, f (fold n l) c) in
+    let po = Option.map (fun (nas, po) -> nas, (f (fold nas l) po)) po in
+    PCase (ci,po,f l p, List.map map_branch pl)
   | PProj (p,pc) -> PProj (p, f l pc)
   | PFix (lni,(lna,tl,bl)) ->
      let l' = Array.fold_left (fun l na -> g na l) l lna in
@@ -352,7 +361,11 @@ let rec subst_pattern env sigma subst pat =
       let ind = cip.cip_ind in
       let ind' = Option.Smart.map (subst_ind subst) ind in
       let cip' = if ind' == ind then cip else { cip with cip_ind = ind' } in
-      let typ' = subst_pattern env sigma subst typ in
+      let map ((nas, typ) as t) =
+        let typ' = subst_pattern env sigma subst typ in
+        if typ' == typ then t else (nas, typ')
+      in
+      let typ' = Option.Smart.map map typ in
       let c' = subst_pattern env sigma subst c in
       let subst_branch ((i,n,c) as br) =
         let c' = subst_pattern env sigma subst c in
@@ -382,8 +395,6 @@ let rec subst_pattern env sigma subst pat =
 let mkPLetIn na b t c = PLetIn(na,b,t,c)
 let mkPProd na t u = PProd(na,t,u)
 let mkPLambda na t b = PLambda(na,t,b)
-let mkPLambdaUntyped na b = PLambda(na,PMeta None,b)
-let rev_it_mkPLambdaUntyped = List.fold_right mkPLambdaUntyped
 
 let mkPProd_or_LetIn (na,_,bo,t) c =
   match bo with
@@ -446,18 +457,14 @@ let rec pat_of_raw metas vars = DAst.with_loc_val (fun ?loc -> function
       PIf (pat_of_raw metas vars c,
            pat_of_raw metas vars b1,pat_of_raw metas vars b2)
   | GLetTuple (nal,(_,None),b,c) ->
-      let mkGLambda na c = DAst.make ?loc @@
-        GLambda (na,Explicit, DAst.make @@ GHole (Evar_kinds.InternalHole, Namegen.IntroAnonymous, None),c) in
-      let c = List.fold_right mkGLambda nal c in
       let cip =
         { cip_style = LetStyle;
           cip_ind = None;
-          cip_ind_tags = None;
           cip_extensible = false }
       in
-      let tags = List.map (fun _ -> false) nal (* Approximation which can be without let-ins... *) in
-      PCase (cip, PMeta None, pat_of_raw metas vars b,
-             [0,tags,pat_of_raw metas vars c])
+      let tags = Array.of_list nal (* Approximation which can be without let-ins... *) in
+      PCase (cip, None, pat_of_raw metas vars b,
+             [0,tags,pat_of_raw metas (List.rev_append (Array.to_list tags) vars) c])
   | GCases (sty,p,[c,(na,indnames)],brs) ->
       let get_ind p = match DAst.get p with
       | PatCstr((ind,_),_,_) -> Some ind
@@ -476,18 +483,17 @@ let rec pat_of_raw metas vars = DAst.with_loc_val (fun ?loc -> function
       let pred = match p,indnames with
         | Some p, Some {CAst.v=(_,nal)} ->
           let nvars = na :: List.rev nal @ vars in
-          rev_it_mkPLambdaUntyped nal (mkPLambdaUntyped na (pat_of_raw metas nvars p))
-        | None, _ -> PMeta None
+          Some (Array.rev_of_list (na :: List.rev nal), pat_of_raw metas nvars p)
+        | None, _ -> None
         | Some p, None ->
           match DAst.get p with
-          | GHole _ -> PMeta None
+          | GHole _ -> None
           | _ ->
             user_err ?loc  (strbrk "Clause \"in\" expected in patterns over \"match\" expressions with an explicit \"return\" clause.")
       in
       let info =
         { cip_style = sty;
           cip_ind = ind;
-          cip_ind_tags = None;
           cip_extensible = ext }
       in
       (* Nota : when we have a non-trivial predicate,
@@ -556,10 +562,10 @@ and pats_of_glob_branches loc metas vars ind brs =
           err ?loc
             (str "No unique branch for " ++ int j ++ str"-th constructor.");
         let lna = List.map get_arg lv in
-        let vars' = List.rev lna @ vars in
-        let pat = rev_it_mkPLambdaUntyped lna (pat_of_raw metas vars' br) in
+        let vars' = List.rev_append lna vars in
+        let tags = Array.of_list lna in
+        let pat = pat_of_raw metas vars' br in
         let ext,pats = get_pat (Int.Set.add (j-1) indexes) brs in
-        let tags = List.map (fun _ -> false) lv (* approximation, w/o let-in *) in
         ext, ((j-1, tags, pat) :: pats)
       | _ ->
         err ?loc:loc' (Pp.str "Non supported pattern.")
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";
diff --git a/user-contrib/Ltac2/g_ltac2.mlg b/user-contrib/Ltac2/g_ltac2.mlg
index 65b61a0d93..548e12d611 100644
--- a/user-contrib/Ltac2/g_ltac2.mlg
+++ b/user-contrib/Ltac2/g_ltac2.mlg
@@ -213,7 +213,7 @@ GRAMMAR EXTEND Gram
       | IDENT "constr"; ":"; "("; c = Constr.lconstr; ")" -> { Tac2quote.of_constr c }
       | IDENT "open_constr"; ":"; "("; c = Constr.lconstr; ")" -> { Tac2quote.of_open_constr c }
       | IDENT "ident"; ":"; "("; c = lident; ")" -> { Tac2quote.of_ident c }
-      | IDENT "pattern"; ":"; "("; c = Constr.cpattern; ")" -> { inj_pattern loc c }
+      | IDENT "pat"; ":"; "("; c = Constr.cpattern; ")" -> { inj_pattern loc c }
       | IDENT "reference"; ":"; "("; c = globref; ")" -> { inj_reference loc c }
       | IDENT "ltac1"; ":"; "("; qid = ltac1_expr_in_env; ")" -> { inj_ltac1 loc qid }
       | IDENT "ltac1val"; ":"; "("; qid = ltac1_expr_in_env; ")" -> { inj_ltac1val loc qid }
diff --git a/user-contrib/Ltac2/tac2core.ml b/user-contrib/Ltac2/tac2core.ml
index 64a2b24404..241ca7ad66 100644
--- a/user-contrib/Ltac2/tac2core.ml
+++ b/user-contrib/Ltac2/tac2core.ml
@@ -1151,7 +1151,7 @@ let () =
     let sigma = Evd.from_env env in
     Patternops.subst_pattern env sigma subst c
   in
-  let print env sigma pat = str "pattern:(" ++ Printer.pr_lconstr_pattern_env env sigma pat ++ str ")" in
+  let print env sigma pat = str "pat:(" ++ Printer.pr_lconstr_pattern_env env sigma pat ++ str ")" in
   let interp _ c = return (Value.of_pattern c) in
   let obj = {
     ml_intern = intern;
diff --git a/user-contrib/Ltac2/tac2print.ml b/user-contrib/Ltac2/tac2print.ml
index fe62de1fb3..a54eb45f61 100644
--- a/user-contrib/Ltac2/tac2print.ml
+++ b/user-contrib/Ltac2/tac2print.ml
@@ -466,7 +466,7 @@ end
 let () = register_init "pattern" begin fun env sigma c ->
   let c = to_pattern c in
   let c = try Printer.pr_lconstr_pattern_env env sigma c with _ -> str "..." in
-  str "pattern:(" ++ c ++ str ")"
+  str "pat:(" ++ c ++ str ")"
 end
 
 let () = register_init "message" begin fun _ _ pp ->