87 files changed, 1100 insertions, 285 deletions

diff --git a/test-suite/bugs/closed/bug_13413.v b/test-suite/bugs/closed/bug_13413.v
new file mode 100644
index 0000000000..b4414a6a1d
--- /dev/null
+++ b/test-suite/bugs/closed/bug_13413.v
@@ -0,0 +1,20 @@
+Goal forall (A B : Prop) (H : A -> B), A -> A -> B.
+intros A B H ?%H H0.
+exact H1.
+Qed.
+
+Goal forall (A B : Prop) (H : A -> B), A -> A -> B.
+intros A B H ?H%H H0.
+exact H1.
+Qed.
+
+Goal forall (A B : Prop) (H : A -> B), A -> A -> B.
+intros A B H J%H H0.
+exact J.
+Qed.
+
+Set Mangle Names.
+Goal forall (A B : Prop) (H : A -> B), A -> A -> B.
+intros A B H ?%H _0.
+assumption.
+Qed.
diff --git a/test-suite/bugs/closed/bug_13755.v b/test-suite/bugs/closed/bug_13755.v
new file mode 100644
index 0000000000..cc25157b9b
--- /dev/null
+++ b/test-suite/bugs/closed/bug_13755.v
@@ -0,0 +1,5 @@
+Module M1.
+Lemma t1 : True.
+Fail End M1.
+Proof. exact I. Qed.
+End M1.
diff --git a/test-suite/bugs/opened/bug_3166.v b/test-suite/bugs/closed/bug_3166.v
index baf87631f0..3b3375fdd8 100644
--- a/test-suite/bugs/opened/bug_3166.v
+++ b/test-suite/bugs/closed/bug_3166.v
@@ -80,5 +80,5 @@ Goal forall T (x y : T) (p : x = y), True.
         ) as H0.
   compute in H0.
   change (fun (x' : T) (_ : y = x') => x' = y) with ((fun y => fun (x' : T) (_ : y = x') => x' = y) y) in H0.
-  Fail pose proof (fun k => @eq_trans _ _ _ k H0).
+  pose proof (fun k => @eq_trans _ _ _ k H0).
 Abort.
diff --git a/test-suite/bugs/closed/bug_4787.v b/test-suite/bugs/closed/bug_4787.v
deleted file mode 100644
index a1444a4f63..0000000000
--- a/test-suite/bugs/closed/bug_4787.v
+++ /dev/null
@@ -1,7 +0,0 @@
-(* [Unset Bracketing Last Introduction Pattern] was not working *)
-
-Unset Bracketing Last Introduction Pattern.
-
-Goal forall T (x y : T * T), fst x = fst y /\ snd x = snd y -> x = y.
-do 10 ((intros [] || intro); simpl); reflexivity.
-Qed.
diff --git a/test-suite/bugs/closed/bug_6157.v b/test-suite/bugs/closed/bug_6157.v
new file mode 100644
index 0000000000..cd24e4c7ee
--- /dev/null
+++ b/test-suite/bugs/closed/bug_6157.v
@@ -0,0 +1,15 @@
+(* Check that universe instances of refs are preserved *)
+
+Section U.
+Set Universe Polymorphism.
+Definition U@{i} := Type@{i}.
+
+Section foo.
+Universe i.
+Fail Check U@{i} : U@{i}.
+Notation Ui := U@{i}. (* syndef path *)
+Fail Check Ui : Type@{i}.
+Notation "#" := U@{i}. (* non-syndef path *)
+Fail Check # : Type@{i}.
+End foo.
+End U.
diff --git a/test-suite/coqdoc/verbatim.html.out b/test-suite/coqdoc/verbatim.html.out
index bf9f975ee8..070f80e771 100644
--- a/test-suite/coqdoc/verbatim.html.out
+++ b/test-suite/coqdoc/verbatim.html.out
@@ -90,7 +90,7 @@ verbatim
 <tr class="infruleassumption">
   <td class="infrule">Γ ⊢ A ∨ B</td>
   <td></td>
-</td>
+</tr>
 </table></center>
 <div class="paragraph"> </div>
 
diff --git a/test-suite/dune b/test-suite/dune
index 6ab2988331..1864153021 100644
--- a/test-suite/dune
+++ b/test-suite/dune
@@ -9,6 +9,10 @@
  (action (with-stdout-to %{targets} (run ./ocaml_pwd.exe -quoted ../../install/%{context_name}/lib/coq/ ))))
 
 (rule
+ (targets bin.inc)
+ (action (with-stdout-to %{targets} (run ./ocaml_pwd.exe -quoted -trailing-slash ../../install/%{context_name}/bin/ ))))
+
+(rule
  (targets summary.log)
  (deps
    ; File that should be promoted.
@@ -44,4 +48,4 @@
    ; %{bin:fake_ide}
  (action
   (progn
-   (bash "make -j %{env:NJOBS=2} BIN= COQLIB=%{read:libpath.inc} PRINT_LOGS=1 UNIT_TESTS=%{env:COQ_UNIT_TEST=unit-tests}"))))
+   (bash "make -j %{env:NJOBS=2} BIN=%{read:bin.inc} COQLIB=%{read:libpath.inc} PRINT_LOGS=1 UNIT_TESTS=%{env:COQ_UNIT_TEST=unit-tests}"))))
diff --git a/test-suite/ltac2/compat.v b/test-suite/ltac2/compat.v
index 9c11d19c27..b50371386f 100644
--- a/test-suite/ltac2/compat.v
+++ b/test-suite/ltac2/compat.v
@@ -40,6 +40,67 @@ Fail Ltac1.run (ltac1val:(x |- idtac) 0).
 Ltac1.run (ltac1val:(x |- idtac x) (Ltac1.of_constr constr:(Type))).
 Abort.
 
+(** Check value-returning FFI *)
+
+(* A dummy CPS wrapper in Ltac1 *)
+Ltac arg k :=
+match goal with
+| [ |- ?P ] => k P
+end.
+
+Ltac2 testeval v :=
+  let r := { contents := None } in
+  let k c :=
+    let () := match Ltac1.to_constr c with
+    | None => ()
+    | Some c => r.(contents) := Some c
+    end in
+    (* dummy return value *)
+    ltac1val:(idtac)
+  in
+  let tac := ltac1val:(arg) in
+  let () := Ltac1.apply tac [Ltac1.lambda k] (fun _ => ()) in
+  match r.(contents) with
+  | None => fail
+  | Some c => if Constr.equal v c then () else fail
+  end.
+
+Goal True.
+Proof.
+testeval 'True.
+Abort.
+
+Goal nat.
+Proof.
+testeval 'nat.
+Abort.
+
+(* CPS towers *)
+Ltac2 testeval2 tac :=
+  let fail _ := Control.zero Not_found in
+  let cast c := match Ltac1.to_constr c with
+  | None => fail ()
+  | Some c => c
+  end in
+  let f x y z :=
+    let x := cast x in
+    let y := cast y in
+    let z := cast z in
+    Ltac1.of_constr constr:($x $y $z)
+  in
+  let f := Ltac1.lambda (fun x => Ltac1.lambda (fun y => Ltac1.lambda (fun z => f x y z))) in
+  Ltac1.apply tac [f] Ltac1.run.
+
+Goal False -> True.
+Proof.
+ltac1:(
+let ff := ltac2:(tac |- testeval2 tac) in
+ff ltac:(fun k =>
+  let c := k (fun (n : nat) (i : True) (e : False) => i) O I in
+  exact c)
+).
+Qed.
+
 (** Test calls to Ltac2 from Ltac1 *)
 
 Set Default Proof Mode "Classic".
diff --git a/test-suite/micromega/reify_bool.v b/test-suite/micromega/reify_bool.v
new file mode 100644
index 0000000000..501fafc0b3
--- /dev/null
+++ b/test-suite/micromega/reify_bool.v
@@ -0,0 +1,18 @@
+Require Import ZArith.
+Require Import Lia.
+Import Z.
+Unset Lia Cache.
+
+Goal forall (x y : Z),
+   implb (Z.eqb x y) (Z.eqb y x) = true.
+Proof.
+  intros.
+  lia.
+Qed.
+
+Goal forall (x y :Z), implb (Z.eqb x 0) (Z.eqb y 0) = true <->
+                      orb (negb (Z.eqb x 0))(Z.eqb y 0) = true.
+Proof.
+  intro.
+  lia.
+Qed.
diff --git a/test-suite/misc/coq_environment.sh b/test-suite/misc/coq_environment.sh
new file mode 100755
index 0000000000..667d11f89e
--- /dev/null
+++ b/test-suite/misc/coq_environment.sh
@@ -0,0 +1,51 @@
+#!/usr/bin/env bash
+
+export COQBIN=$BIN
+export PATH=$COQBIN:$PATH
+
+TMP=`mktemp -d`
+cd $TMP
+
+cat > coq_environment.txt <<EOT
+# we override COQLIB because we can
+COQLIB="$TMP/overridden" # bla bla
+OCAMLFIND="$TMP/overridden"
+FOOBAR="one more"
+EOT
+
+cp $BIN/coqc .
+cp $BIN/coq_makefile .
+mkdir -p overridden/tools/
+cp $COQLIB/tools/CoqMakefile.in overridden/tools/
+
+unset COQLIB
+N=`./coqc -config | grep COQLIB | grep /overridden | wc -l`
+if [ $N -ne 1 ]; then
+  echo COQLIB not overridden by coq_environment
+  coqc -config
+  exit 1
+fi
+N=`./coqc -config | grep OCAMLFIND | grep /overridden | wc -l`
+if [ $N -ne 1 ]; then
+  echo OCAMLFIND not overridden by coq_environment
+  coqc -config
+  exit 1
+fi
+./coq_makefile -o CoqMakefile -R . foo > /dev/null
+N=`grep COQMF_OCAMLFIND CoqMakefile.conf | grep /overridden | wc -l`
+if [ $N -ne 1 ]; then
+  echo COQMF_OCAMLFIND not overridden by coq_environment
+  cat CoqMakefile.conf
+  exit 1
+fi
+
+export COQLIB="/overridden2"
+N=`./coqc -config | grep COQLIB | grep /overridden2 | wc -l`
+if [ $N -ne 1 ]; then
+  echo COQLIB not overridden by COQLIB when coq_environment present
+  coqc -config
+  exit 1
+fi
+
+rm -rf $TMP
+exit 0
diff --git a/test-suite/misc/non-marshalable-state.sh b/test-suite/misc/non-marshalable-state.sh
new file mode 100755
index 0000000000..eef7786ebc
--- /dev/null
+++ b/test-suite/misc/non-marshalable-state.sh
@@ -0,0 +1,30 @@
+#!/usr/bin/env bash
+
+set -e
+
+export COQBIN=$BIN
+export PATH=$COQBIN:$PATH
+
+cd misc/non-marshalable-state/
+
+coq_makefile -f _CoqProject -o Makefile
+
+make clean
+
+make src/evil_plugin.cmxs
+make src/good_plugin.cmxs
+
+RC=1
+# must fail
+coqc -async-proofs on  -I src -Q theories Marshal theories/evil.v 2> log1 1>&2 || RC=0
+#   for this reason
+grep -q 'Marshalling error' log1 || RC=1
+
+# must work
+coqc -async-proofs off -I src -Q theories Marshal theories/evil.v
+
+# must work
+coqc -async-proofs on  -I src -Q theories Marshal theories/good.v
+
+
+exit $RC
diff --git a/test-suite/misc/non-marshalable-state/_CoqProject b/test-suite/misc/non-marshalable-state/_CoqProject
new file mode 100644
index 0000000000..09e68d866c
--- /dev/null
+++ b/test-suite/misc/non-marshalable-state/_CoqProject
@@ -0,0 +1,9 @@
+-Q theories Marshal
+-I src
+
+src/evil.mlg
+src/good.mlg
+src/evil_plugin.mlpack
+src/good_plugin.mlpack
+theories/evil.v
+theories/good.v
diff --git a/test-suite/misc/non-marshalable-state/src/evil.mlg b/test-suite/misc/non-marshalable-state/src/evil.mlg
new file mode 100644
index 0000000000..59b2b5a8ac
--- /dev/null
+++ b/test-suite/misc/non-marshalable-state/src/evil.mlg
@@ -0,0 +1,15 @@
+DECLARE PLUGIN "evil_plugin"
+
+{
+
+let state = Summary.ref
+  ~name:"elpi-compiler-cache"
+  None
+
+}
+
+VERNAC COMMAND EXTEND magic CLASSIFIED AS SIDEFF
+| [ "magic" ] -> {
+    state := Some (fun () -> ())
+}
+END
diff --git a/test-suite/misc/non-marshalable-state/src/evil_plugin.mlpack b/test-suite/misc/non-marshalable-state/src/evil_plugin.mlpack
new file mode 100644
index 0000000000..6382aa69e1
--- /dev/null
+++ b/test-suite/misc/non-marshalable-state/src/evil_plugin.mlpack
@@ -0,0 +1 @@
+Evil
diff --git a/test-suite/misc/non-marshalable-state/src/good.mlg b/test-suite/misc/non-marshalable-state/src/good.mlg
new file mode 100644
index 0000000000..c6b9cbefd5
--- /dev/null
+++ b/test-suite/misc/non-marshalable-state/src/good.mlg
@@ -0,0 +1,16 @@
+DECLARE PLUGIN "good_plugin"
+
+{
+
+let state = Summary.Local.ref
+  ~name:"elpi-compiler-cache"
+  None
+
+}
+
+VERNAC COMMAND EXTEND magic CLASSIFIED AS SIDEFF
+| [ "magic" ] -> {
+    let open Summary.Local in
+    state := Some (fun () -> ())
+}
+END
diff --git a/test-suite/misc/non-marshalable-state/src/good_plugin.mlpack b/test-suite/misc/non-marshalable-state/src/good_plugin.mlpack
new file mode 100644
index 0000000000..cd9dd73b78
--- /dev/null
+++ b/test-suite/misc/non-marshalable-state/src/good_plugin.mlpack
@@ -0,0 +1 @@
+Good
diff --git a/test-suite/misc/non-marshalable-state/theories/evil.v b/test-suite/misc/non-marshalable-state/theories/evil.v
new file mode 100644
index 0000000000..661482a975
--- /dev/null
+++ b/test-suite/misc/non-marshalable-state/theories/evil.v
@@ -0,0 +1,5 @@
+Declare ML Module "evil_plugin".
+
+magic.
+
+Lemma x : True. Proof. trivial. Qed.
diff --git a/test-suite/misc/non-marshalable-state/theories/good.v b/test-suite/misc/non-marshalable-state/theories/good.v
new file mode 100644
index 0000000000..eab9a043e1
--- /dev/null
+++ b/test-suite/misc/non-marshalable-state/theories/good.v
@@ -0,0 +1,5 @@
+Declare ML Module "good_plugin".
+
+magic.
+
+Lemma x : True. Proof. trivial. Qed.
diff --git a/test-suite/ocaml_pwd.ml b/test-suite/ocaml_pwd.ml
index afa3deea3a..054a921b93 100644
--- a/test-suite/ocaml_pwd.ml
+++ b/test-suite/ocaml_pwd.ml
@@ -1,7 +1,26 @@
+open Arg
+
+let quoted = ref false
+let trailing_slash = ref false
+
+let arguments = [
+  "-quoted",Set quoted, "Quote path";
+  "-trailing-slash",Set trailing_slash, "End the path with a /";
+]
+let subject = ref None
+let set_subject x =
+  if !subject <> None then
+    failwith "only one path";
+  subject := Some x
+
 let _ =
-  let quoted = Sys.argv.(1) = "-quoted" in
-  let ch_dir = Sys.argv.(if quoted then 2 else 1) in
-  Sys.chdir ch_dir;
+  Arg.parse arguments set_subject "Usage:";
+  let subject =
+    match !subject with
+    | None -> failwith "no path given";
+    | Some x -> x in
+  Sys.chdir subject;
   let dir = Sys.getcwd () in
-  let dir = if quoted then Filename.quote dir else dir in
+  let dir = if !trailing_slash then dir ^ "/" else dir in
+  let dir = if !quoted then Filename.quote dir else dir in
   Format.printf "%s%!" dir
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/Arguments_renaming.out b/test-suite/output/Arguments_renaming.out
index e46774f68a..9fd846ac16 100644
--- a/test-suite/output/Arguments_renaming.out
+++ b/test-suite/output/Arguments_renaming.out
@@ -11,7 +11,7 @@ eq_refl
      : ?y = ?y
 where
 ?y : [ |- nat]
-Inductive eq (A : Type) (x : A) : A -> Prop :=  eq_refl : x = x
+Inductive eq (A : Type) (x : A) : A -> Prop :=  eq_refl : x = x.
 
 Arguments eq {A}%type_scope _ _
 Arguments eq_refl {B}%type_scope {y}, [_] _
@@ -22,7 +22,7 @@ eq_refl is not universe polymorphic
 Arguments eq_refl {B}%type_scope {y}, [_] _
   (where some original arguments have been renamed)
 Expands to: Constructor Coq.Init.Logic.eq_refl
-Inductive myEq (B : Type) (x : A) : A -> Prop :=  myrefl : B -> myEq B x x
+Inductive myEq (B : Type) (x : A) : A -> Prop :=  myrefl : B -> myEq B x x.
 
 Arguments myEq _%type_scope _ _
 Arguments myrefl {C}%type_scope x _
@@ -55,7 +55,7 @@ Expands to: Constant Arguments_renaming.Test1.myplus
 @myplus
      : forall Z : Type, Z -> nat -> nat -> nat
 Inductive myEq (A B : Type) (x : A) : A -> Prop :=
-    myrefl : B -> myEq A B x x
+    myrefl : B -> myEq A B x x.
 
 Arguments myEq (_ _)%type_scope _ _
 Arguments myrefl A%type_scope {C}%type_scope x _
diff --git a/test-suite/output/Cases.out b/test-suite/output/Cases.out
index 01564e7f25..ea647a990a 100644
--- a/test-suite/output/Cases.out
+++ b/test-suite/output/Cases.out
@@ -50,10 +50,11 @@ f =
 fun H : B =>
 match H with
 | AC x =>
-    let b0 := b in
-    (if b0 as b return (P b -> True)
-     then fun _ : P true => Logic.I
-     else fun _ : P false => Logic.I) x
+    (fun x0 : P b =>
+     let b0 := b in
+     (if b0 as b return (P b -> True)
+      then fun _ : P true => Logic.I
+      else fun _ : P false => Logic.I) x0) x
 end
      : B -> True
 The command has indeed failed with message:
@@ -74,7 +75,9 @@ fun '{{n, m, p}} => n + m + p
 fun '(D n m p q) => n + m + p + q
      : J -> nat
 The command has indeed failed with message:
-The constructor D (in type J) expects 3 arguments.
+Once notations are expanded, the resulting constructor D (in type J) is
+expected to be applied to no arguments while it is actually applied to
+1 argument.
 lem1 = 
 fun dd : nat * nat => let (bb, cc) as aa return (aa = aa) := dd in eq_refl
      : forall k : nat * nat, k = k
@@ -86,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
@@ -106,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,
@@ -181,3 +184,51 @@ end
 File "stdin", line 253, characters 4-5:
 Warning: Unused variable B catches more than one case.
 [unused-pattern-matching-variable,pattern-matching]
+The command has indeed failed with message:
+Application of arguments to a recursive notation not supported in patterns.
+The command has indeed failed with message:
+The constructor cons (in type list) is expected to be applied to 2 arguments
+while it is actually applied to 3 arguments.
+The command has indeed failed with message:
+The constructor cons (in type list) is expected to be applied to 2 arguments
+while it is actually applied to 1 argument.
+The command has indeed failed with message:
+The constructor D' (in type J') is expected to be applied to 4 arguments (or
+6 arguments when including variables for local definitions) while it is
+actually applied to 5 arguments.
+fun x : J' bool (true, true) =>
+match x with
+| D' _ _ _ m _ e => existT (fun x0 : nat => x0 = x0) m e
+end
+     : J' bool (true, true) -> {x0 : nat & x0 = x0}
+fun x : J' bool (true, true) =>
+match x with
+| @D' _ _ _ _ n _ p _ => n + p
+end
+     : J' bool (true, true) -> nat
+The command has indeed failed with message:
+Application of arguments to a recursive notation not supported in patterns.
+The command has indeed failed with message:
+The constructor cons (in type list) is expected to be applied to 2 arguments
+while it is actually applied to 3 arguments.
+The command has indeed failed with message:
+The constructor cons (in type list) is expected to be applied to 2 arguments
+while it is actually applied to 1 argument.
+The command has indeed failed with message:
+The constructor D' (in type J') is expected to be applied to 3 arguments (or
+4 arguments when including variables for local definitions) while it is
+actually applied to 2 arguments.
+The command has indeed failed with message:
+The constructor D' (in type J') is expected to be applied to 3 arguments (or
+4 arguments when including variables for local definitions) while it is
+actually applied to 5 arguments.
+fun x : J' bool (true, true) =>
+match x with
+| @D' _ _ _ _ _ m _ e => existT (fun x0 : nat => x0 = x0) m e
+end
+     : J' bool (true, true) -> {x0 : nat & x0 = x0}
+fun x : J' bool (true, true) =>
+match x with
+| @D' _ _ _ _ n _ p _ => (n, p)
+end
+     : J' bool (true, true) -> nat * nat
diff --git a/test-suite/output/Cases.v b/test-suite/output/Cases.v
index 2d8a8b359c..0cb3ac3ddc 100644
--- a/test-suite/output/Cases.v
+++ b/test-suite/output/Cases.v
@@ -254,3 +254,33 @@ Definition bar (f : foo) :=
   end.
 
 End Wish12762.
+
+Module ConstructorArgumentsNumber.
+
+Arguments cons {A} _ _.
+
+Inductive J' A {B} (C:=(A*B)%type) (c:C) := D' : forall n {m}, let p := n+m in m=m -> J' A c.
+
+Unset Asymmetric Patterns.
+
+Fail Check fun x => match x with (y,z) w => y+z+w end.
+Fail Check fun x => match x with cons y z w => 0 | nil => 0 end.
+Fail Check fun x => match x with cons y => 0 | nil => 0 end.
+
+(* Missing a let-in to be in let-in mode *)
+Fail Check fun x => match x with D' _ _ n p e => 0 end.
+Check fun x : J' bool (true,true) => match x with D' _ _ n e => existT (fun x => eq x x) _ e end.
+Check fun x : J' bool (true,true) => match x with D' _ _ _ n p e => n+p end.
+
+Set Asymmetric Patterns.
+
+Fail Check fun x => match x with (y,z) w => y+z+w end.
+Fail Check fun x => match x with cons y z w => 0 | nil => 0 end.
+Fail Check fun x => match x with cons y => 0 | nil => 0 end.
+
+Fail Check fun x => match x with D' n _ => 0 end.
+Fail Check fun x => match x with D' n m p e _ => 0 end.
+Check fun x : J' bool (true,true) => match x with D' n m e => existT (fun x => eq x x) m e end.
+Check fun x : J' bool (true,true) => match x with D' n m p e => (n,p) end.
+
+End ConstructorArgumentsNumber.
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/Function.out b/test-suite/output/Function.out
new file mode 100644
index 0000000000..e69de29bb2
--- /dev/null
+++ b/test-suite/output/Function.out
diff --git a/test-suite/output/Function.v b/test-suite/output/Function.v
new file mode 100644
index 0000000000..b3e2a93895
--- /dev/null
+++ b/test-suite/output/Function.v
@@ -0,0 +1,31 @@
+Require Import FunInd List.
+
+(* Explanations: This kind of pattern matching displays a legitimate
+   unused variable warning in v8.13.
+
+Fixpoint f (l:list nat) : nat :=
+  match l with
+  | nil => O
+  | S n :: nil  => 1
+  | x :: l'  => f l'
+  end.
+*)
+
+(* In v8.13 the same code with "Function" generates a lot more
+   warnings about variables created automatically by Function. These
+   are not legitimate. PR #13776 (post v8.13) removes all warnings
+   about pattern matching variables (and non truly recursive fixpoint)
+   for "Function". So this should not generate any warning. Note that
+   this PR removes also the legitimate warnings. It would be better if
+   this test generate the same warning as the Fixpoint above. This
+   test would then need to be updated. *)
+
+(* Ensuring the warning is a warning. *)
+Set Warnings "matching-variable".
+(* But no warning generated here. *)
+Function f (l:list nat) : nat :=
+  match l with
+  | nil => O
+  | S n :: nil  => 1
+  | n :: l'  => f l'
+  end.
diff --git a/test-suite/output/Inductive.out b/test-suite/output/Inductive.out
index 8e10107673..fc3b6fbd99 100644
--- a/test-suite/output/Inductive.out
+++ b/test-suite/output/Inductive.out
@@ -5,7 +5,7 @@ A : Set
 a : A
 l : list' A
 Unable to unify "list' (A * A)%type" with "list' A".
-Inductive foo (A : Type) (x : A) (y : A := x) : Prop :=  Foo : foo A x
+Inductive foo (A : Type) (x : A) (y : A := x) : Prop :=  Foo : foo A x.
 
 Arguments foo _%type_scope _
 Arguments Foo _%type_scope _
diff --git a/test-suite/output/InitSyntax.out b/test-suite/output/InitSyntax.out
index 02e58775b5..fdd609f5b2 100644
--- a/test-suite/output/InitSyntax.out
+++ b/test-suite/output/InitSyntax.out
@@ -1,5 +1,5 @@
 Inductive sig2 (A : Type) (P Q : A -> Prop) : Type :=
-    exist2 : forall x : A, P x -> Q x -> {x : A | P x & Q x}
+    exist2 : forall x : A, P x -> Q x -> {x : A | P x & Q x}.
 
 Arguments sig2 [A]%type_scope (_ _)%type_scope
 Arguments exist2 [A]%type_scope (_ _)%function_scope _ _ _
diff --git a/test-suite/output/Int63Syntax.out b/test-suite/output/Int63Syntax.out
index eefa338f0d..7ca4de1e46 100644
--- a/test-suite/output/Int63Syntax.out
+++ b/test-suite/output/Int63Syntax.out
@@ -1,7 +1,5 @@
 2%int63
      : int
-(2 + 2)%int63
-     : int
 2
      : int
 9223372036854775807
@@ -17,9 +15,9 @@
 427
      : int
 The command has indeed failed with message:
-Cannot interpret this number as a value of type Coq.Numbers.Cyclic.Int63.Int63.int
+Cannot interpret this number as a value of type Coq.Numbers.Cyclic.Int63.PrimInt63.int
 The command has indeed failed with message:
-Cannot interpret this number as a value of type Coq.Numbers.Cyclic.Int63.Int63.int
+Cannot interpret this number as a value of type Coq.Numbers.Cyclic.Int63.PrimInt63.int
 0
      : int
 0
@@ -32,13 +30,7 @@ The command has indeed failed with message:
 The reference x1 was not found in the current environment.
 The command has indeed failed with message:
 The reference x was not found in the current environment.
-2 + 2
-     : int
-2 + 2
-     : int
-     = 4
-     : int
-     = 37151199385380486
+add 2 2
      : int
 The command has indeed failed with message:
 int63 are only non-negative numbers.
@@ -56,3 +48,29 @@ t = 2%i63
      : nat
 2
      : int
+(2 + 2)%int63
+     : int
+2 + 2
+     : int
+     = 4
+     : int
+     = 37151199385380486
+     : int
+     = 4
+     : int
+     = 4
+     : int
+     = 4
+     : int
+     = add
+     : int -> int -> int
+     = 12
+     : int
+     = 12
+     : int
+     = 12
+     : int
+     = 3 + x
+     : int
+     = 1 + 2 + x
+     : int
diff --git a/test-suite/output/Int63Syntax.v b/test-suite/output/Int63Syntax.v
index c49616d918..50910264f2 100644
--- a/test-suite/output/Int63Syntax.v
+++ b/test-suite/output/Int63Syntax.v
@@ -1,7 +1,6 @@
-Require Import Int63 Cyclic63.
+Require Import PrimInt63.
 
 Check 2%int63.
-Check (2 + 2)%int63.
 Open Scope int63_scope.
 Check 2.
 Check 9223372036854775807.
@@ -18,10 +17,7 @@ Fail Check 0xg.
 Fail Check 0xG.
 Fail Check 00x1.
 Fail Check 0x.
-Check (Int63.add 2 2).
-Check (2+2).
-Eval vm_compute in 2+2.
-Eval vm_compute in 65675757 * 565675998.
+Check (PrimInt63.add 2 2).
 Fail Check -1.
 Fail Check 9223372036854775808.
 Open Scope nat_scope.
@@ -36,3 +32,26 @@ Check 2.
 Close Scope nat_scope.
 Check 2.
 Close Scope int63_scope.
+
+Require Import Int63.
+
+Check (2 + 2)%int63.
+Open Scope int63_scope.
+Check (2+2).
+Eval vm_compute in 2+2.
+Eval vm_compute in 65675757 * 565675998.
+
+Eval simpl in 2+2.
+Eval hnf in 2+2.
+Eval cbn in 2+2.
+Eval hnf in PrimInt63.add.
+
+Eval simpl in (2 * 3) + (2 * 3).
+Eval hnf in (2 * 3) + (2 * 3).
+Eval cbn in (2 * 3) + (2 * 3).
+
+Section TestNoSimpl.
+Variable x : int.
+Eval simpl in 1 + 2 + x.
+Eval hnf in 1 + 2 + x.
+End TestNoSimpl.
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/PrintInfos.out b/test-suite/output/PrintInfos.out
index fe16dba496..03b9e3b527 100644
--- a/test-suite/output/PrintInfos.out
+++ b/test-suite/output/PrintInfos.out
@@ -4,14 +4,14 @@ existT is template universe polymorphic on sigT.u0 sigT.u1
 Arguments existT [A]%type_scope _%function_scope _ _
 Expands to: Constructor Coq.Init.Specif.existT
 Inductive sigT (A : Type) (P : A -> Type) : Type :=
-    existT : forall x : A, P x -> {x : A & P x}
+    existT : forall x : A, P x -> {x : A & P x}.
 
 Arguments sigT [A]%type_scope _%type_scope
 Arguments existT [A]%type_scope _%function_scope _ _
 existT : forall [A : Type] (P : A -> Type) (x : A), P x -> {x : A & P x}
 
 Argument A is implicit
-Inductive eq (A : Type) (x : A) : A -> Prop :=  eq_refl : x = x
+Inductive eq (A : Type) (x : A) : A -> Prop :=  eq_refl : x = x.
 
 Arguments eq {A}%type_scope _ _
 Arguments eq_refl {A}%type_scope {x}, [_] _
@@ -50,7 +50,7 @@ Arguments plus_n_O _%nat_scope
 plus_n_O is opaque
 Expands to: Constant Coq.Init.Peano.plus_n_O
 Inductive le (n : nat) : nat -> Prop :=
-    le_n : n <= n | le_S : forall m : nat, n <= m -> n <= S m
+    le_n : n <= n | le_S : forall m : nat, n <= m -> n <= S m.
 
 Arguments le (_ _)%nat_scope
 Arguments le_n _%nat_scope
@@ -60,7 +60,7 @@ comparison : Set
 comparison is not universe polymorphic
 Expands to: Inductive Coq.Init.Datatypes.comparison
 Inductive comparison : Set :=
-    Eq : comparison | Lt : comparison | Gt : comparison
+    Eq : comparison | Lt : comparison | Gt : comparison.
 bar : foo
 
 bar is not universe polymorphic
@@ -78,7 +78,7 @@ Arguments bar {x}
 Module Coq.Init.Peano
 Notation sym_eq := eq_sym
 Expands to: Notation Coq.Init.Logic.sym_eq
-Inductive eq (A : Type) (x : A) : A -> Prop :=  eq_refl : x = x
+Inductive eq (A : Type) (x : A) : A -> Prop :=  eq_refl : x = x.
 
 Arguments eq {A}%type_scope _ _
 Arguments eq_refl {A}%type_scope {x}, {_} _
diff --git a/test-suite/output/PrintModule.out b/test-suite/output/PrintModule.out
index 1a9bc068c5..7c7600b786 100644
--- a/test-suite/output/PrintModule.out
+++ b/test-suite/output/PrintModule.out
@@ -7,3 +7,11 @@ Module N : S with Module T := K := M
 Module N : S with Module T := M
 
 Module Type Func = Funsig (T0:Test) Sig Parameter x : T0.t. End
+Module
+A
+:= Struct
+     Variant I : Set :=  C : nat -> I.
+     Record R : Set := Build_R { n : nat }.
+     Definition n : R -> nat.
+   End
+
diff --git a/test-suite/output/PrintModule.v b/test-suite/output/PrintModule.v
index 54ef305be4..b4de03b556 100644
--- a/test-suite/output/PrintModule.v
+++ b/test-suite/output/PrintModule.v
@@ -60,3 +60,10 @@ Print Func.
 End Shortest_path.
 
 End QUX.
+
+Module A.
+Variant I := C : nat -> I.
+Record R := { n : nat }.
+End A.
+
+Print Module A.
diff --git a/test-suite/output/RecordFieldErrors.out b/test-suite/output/RecordFieldErrors.out
index 5b67f632c9..b80345108e 100644
--- a/test-suite/output/RecordFieldErrors.out
+++ b/test-suite/output/RecordFieldErrors.out
@@ -11,4 +11,4 @@ This record defines several times the field foo.
 The command has indeed failed with message:
 This record defines several times the field unit.
 The command has indeed failed with message:
-unit: Not a projection of inductive t.
+unit: Not a projection.
diff --git a/test-suite/output/RecordFieldErrors.v b/test-suite/output/RecordFieldErrors.v
index 27aa07822b..ff817c31aa 100644
--- a/test-suite/output/RecordFieldErrors.v
+++ b/test-suite/output/RecordFieldErrors.v
@@ -35,4 +35,4 @@ acceptable and seems an unlikely mistake. *)
 
 Fail Check {| foo := tt;
               unit := tt |}.
-(* unit: Not a projection of inductive t. *)
+(* unit: Not a projection. *)
diff --git a/test-suite/output/SearchHead.v b/test-suite/output/SearchHead.v
deleted file mode 100644
index 2ee8a0d184..0000000000
--- a/test-suite/output/SearchHead.v
+++ /dev/null
@@ -1,19 +0,0 @@
-(* Some tests of the Search command *)
-
-SearchHead le.				(* app nodes *)
-SearchHead bool. 				(* no apps *)
-SearchHead (@eq nat).			(* complex pattern *)
-
-Definition newdef := fun x:nat => x = x.
-
-Goal forall n:nat, newdef n -> False.
-  intros n h.
-  SearchHead newdef.             (* search hypothesis *)
-Abort.
-
-
-Goal forall n (P:nat -> Prop), P n -> False.
-  intros n P h.
-  SearchHead P.                  (* search hypothesis also for patterns *)
-Abort.
-
diff --git a/test-suite/output/SearchHead.out b/test-suite/output/Search_headconcl.out
index 2f0d854ac6..24e2ee76af 100644
--- a/test-suite/output/SearchHead.out
+++ b/test-suite/output/Search_headconcl.out
@@ -1,17 +1,9 @@
-File "stdin", line 3, characters 0-14:
-Warning:
-SearchHead is deprecated. Use the headconcl: clause of Search instead.
-[deprecated-searchhead,deprecated]
 le_n: forall n : nat, n <= n
 le_0_n: forall n : nat, 0 <= n
 le_S: forall n m : nat, n <= m -> n <= S m
 le_pred: forall n m : nat, n <= m -> Nat.pred n <= Nat.pred m
 le_n_S: forall n m : nat, n <= m -> S n <= S m
 le_S_n: forall n m : nat, S n <= S m -> n <= m
-File "stdin", line 4, characters 0-16:
-Warning:
-SearchHead is deprecated. Use the headconcl: clause of Search instead.
-[deprecated-searchhead,deprecated]
 false: bool
 true: bool
 negb: bool -> bool
@@ -35,10 +27,6 @@ Hexadecimal.uint_beq: Hexadecimal.uint -> Hexadecimal.uint -> bool
 Decimal.decimal_beq: Decimal.decimal -> Decimal.decimal -> bool
 Decimal.int_beq: Decimal.int -> Decimal.int -> bool
 Decimal.uint_beq: Decimal.uint -> Decimal.uint -> bool
-File "stdin", line 5, characters 0-21:
-Warning:
-SearchHead is deprecated. Use the headconcl: clause of Search instead.
-[deprecated-searchhead,deprecated]
 mult_n_O: forall n : nat, 0 = n * 0
 plus_O_n: forall n : nat, 0 + n = n
 plus_n_O: forall n : nat, n = n + 0
@@ -57,13 +45,5 @@ f_equal2_plus:
   forall x1 y1 x2 y2 : nat, x1 = y1 -> x2 = y2 -> x1 + x2 = y1 + y2
 f_equal2_mult:
   forall x1 y1 x2 y2 : nat, x1 = y1 -> x2 = y2 -> x1 * x2 = y1 * y2
-File "stdin", line 11, characters 2-20:
-Warning:
-SearchHead is deprecated. Use the headconcl: clause of Search instead.
-[deprecated-searchhead,deprecated]
 h: newdef n
-File "stdin", line 17, characters 2-15:
-Warning:
-SearchHead is deprecated. Use the headconcl: clause of Search instead.
-[deprecated-searchhead,deprecated]
 h: P n
diff --git a/test-suite/output/Search_headconcl.v b/test-suite/output/Search_headconcl.v
new file mode 100644
index 0000000000..8b168dcd25
--- /dev/null
+++ b/test-suite/output/Search_headconcl.v
@@ -0,0 +1,18 @@
+(* Some tests of the Search command *)
+
+Search headconcl: le.				(* app nodes *)
+Search headconcl: bool. 				(* no apps *)
+Search headconcl: (@eq nat).			(* complex pattern *)
+
+Definition newdef := fun x:nat => x = x.
+
+Goal forall n:nat, newdef n -> False.
+  intros n h.
+  Search headconcl: newdef.             (* search hypothesis *)
+Abort.
+
+
+Goal forall n (P:nat -> Prop), P n -> False.
+  intros n P h.
+  Search headconcl: P.                  (* search hypothesis also for patterns *)
+Abort.
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/StringSyntaxPrimitive.out b/test-suite/output/StringSyntaxPrimitive.out
new file mode 100644
index 0000000000..131975c760
--- /dev/null
+++ b/test-suite/output/StringSyntaxPrimitive.out
@@ -0,0 +1,20 @@
+"abc"
+     : intList
+"abc"
+     : intList
+mk_intList [97%int63; 98%int63; 99%int63]
+     : intList
+"abc"
+     : intArray
+"abc"
+     : intArray
+     = "abc"
+     : nestArray
+"abc"
+     : nestArray
+"100"
+     : floatList
+"100"
+     : floatList
+mk_floatList [1%float; 0%float; 0%float]
+     : floatList
diff --git a/test-suite/output/StringSyntaxPrimitive.v b/test-suite/output/StringSyntaxPrimitive.v
new file mode 100644
index 0000000000..23ef082013
--- /dev/null
+++ b/test-suite/output/StringSyntaxPrimitive.v
@@ -0,0 +1,139 @@
+Require Import Coq.Lists.List.
+Require Import Coq.Strings.String Coq.Strings.Byte Coq.Strings.Ascii.
+Require Coq.Array.PArray Coq.Floats.PrimFloat.
+Require Import Coq.Numbers.BinNums Coq.Numbers.Cyclic.Int63.Int63.
+
+Set Printing Depth 100000.
+Set Printing Width 1000.
+
+Close Scope char_scope.
+Close Scope string_scope.
+
+(* Notations for primitive integers inside polymorphic datatypes *)
+Module Test1.
+  Inductive intList := mk_intList (_ : list int).
+  Definition i63_from_byte (b : byte) : int := Int63.of_Z (BinInt.Z.of_N (Byte.to_N b)).
+  Definition i63_to_byte (i : int) : byte :=
+      match Byte.of_N (BinInt.Z.to_N (Int63.to_Z i)) with Some x => x | None => x00%byte end.
+
+  Definition to_byte_list '(mk_intList a) := List.map i63_to_byte a.
+
+  Definition from_byte_list (xs : list byte) : intList:=
+    mk_intList (List.map i63_from_byte xs).
+
+  Declare Scope intList_scope.
+  Delimit Scope intList_scope with intList.
+
+  String Notation intList from_byte_list to_byte_list : intList_scope.
+
+  Open Scope intList_scope.
+  Import List.ListNotations.
+  Check mk_intList [97; 98; 99]%int63%list.
+  Check "abc"%intList.
+
+  Definition int' := int.
+  Check mk_intList (@cons int' 97 [98; 99])%int63%list.
+End Test1.
+
+Import PArray.
+
+(* Notations for primitive arrays *)
+Module Test2.
+  Inductive intArray := mk_intArray (_ : array int).
+
+  Definition i63_from_byte (b : byte) : Int63.int := Int63.of_Z (BinInt.Z.of_N (Byte.to_N b)).
+  Definition i63_to_byte (i : Int63.int) : byte :=
+  match Byte.of_N (BinInt.Z.to_N (Int63.to_Z i)) with Some x => x | None => x00%byte end.
+
+  Definition i63_to_nat x := BinInt.Z.to_nat (Int63.to_Z x).
+  Local Definition nat_length {X} (x : array X) :nat := i63_to_nat (length x).
+
+  Local Fixpoint list_length_i63 {A} (xs : list A) :int :=
+            match xs with
+            | nil => 0
+            | cons _ xs => 1 + list_length_i63 xs
+            end.
+
+  Definition to_byte_list '(mk_intArray a) :=
+    ((fix go (n : nat) (i : Int63.int) (acc : list byte) :=
+        match n with
+        | 0 => acc
+        | S n => go n (i - 1) (cons (i63_to_byte a.[i]) acc)
+        end) (nat_length a) (length a - 1) nil)%int63.
+
+  Definition from_byte_list (xs : list byte) :=
+    (let arr := make (list_length_i63 xs) 0 in
+    mk_intArray ((fix go i xs acc :=
+        match xs with
+        | nil => acc
+        | cons x xs => go (i + 1) xs (acc.[i <- i63_from_byte x])
+        end) 0 xs arr))%int63.
+
+  Declare Scope intArray_scope.
+  Delimit Scope intArray_scope with intArray.
+
+  String Notation intArray from_byte_list to_byte_list : intArray_scope.
+
+  Open Scope intArray_scope.
+  Check mk_intArray ( [| 97; 98; 99 | 0|])%int63%array.
+  Check "abc"%intArray.
+
+End Test2.
+
+(* Primitive arrays inside primitive arrays *)
+Module Test3.
+
+  Inductive nestArray := mk_nestArray (_ : array (array int)).
+  Definition to_byte_list '(mk_nestArray a) :=
+    ((fix go (n : nat) (i : Int63.int) (acc : list byte) :=
+        match n with
+        | 0 => acc
+        | S n => go n (i - 1) (cons (Test2.i63_to_byte a.[i].[0]) acc)
+        end) (Test2.nat_length a) (length a - 1) nil)%int63.
+
+  Definition from_byte_list (xs : list byte) :=
+    (let arr := make (Test2.list_length_i63 xs) (make 0 0) in
+    mk_nestArray ((fix go i xs acc :=
+        match xs with
+        | nil => acc
+        | cons x xs => go (i + 1) xs (acc.[i <- make 1 (Test2.i63_from_byte x)])
+        end) 0 xs arr))%int63.
+
+  Declare Scope nestArray_scope.
+  Delimit Scope nestArray_scope with nestArray.
+
+  String Notation nestArray from_byte_list to_byte_list : nestArray_scope.
+
+  Open Scope nestArray_scope.
+  Eval cbv in mk_nestArray ( [| make 1 97; make 1 98; make 1 99 | make 0 0|])%int63%array.
+  Check "abc"%nestArray.
+End Test3.
+
+
+
+(* Notations for primitive floats inside polymorphic datatypes *)
+Module Test4.
+  Import PrimFloat.
+  Inductive floatList := mk_floatList (_ : list float).
+  Definition float_from_byte (b : byte) : float :=
+    if Byte.eqb b "0"%byte then PrimFloat.zero else PrimFloat.one.
+  Definition float_to_byte (f : float) : byte :=
+    if PrimFloat.is_zero f then "0" else "1".
+  Definition to_byte_list '(mk_floatList a) := List.map float_to_byte a.
+
+  Definition from_byte_list (xs : list byte) : floatList:=
+    mk_floatList (List.map float_from_byte xs).
+
+  Declare Scope floatList_scope.
+  Delimit Scope floatList_scope with floatList.
+
+  String Notation floatList from_byte_list to_byte_list : floatList_scope.
+
+  Open Scope floatList_scope.
+  Import List.ListNotations.
+  Check mk_floatList [97; 0; 0]%float%list.
+  Check "100"%floatList.
+
+  Definition float' := float.
+  Check mk_floatList (@cons float' 1 [0; 0])%float%list.
+End Test4.
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/UnivBinders.out b/test-suite/output/UnivBinders.out
index 0fbb4f4c11..4993b747fa 100644
--- a/test-suite/output/UnivBinders.out
+++ b/test-suite/output/UnivBinders.out
@@ -1,6 +1,7 @@
-Inductive Empty@{uu} : Type@{uu} :=  
+Inductive Empty@{uu} : Type@{uu} :=  .
 (* uu |=  *)
-Record PWrap (A : Type@{uu}) : Type@{uu} := pwrap { punwrap : A }
+Record PWrap (A : Type@{uu}) : Type@{uu} := pwrap
+  { punwrap : A }.
 (* uu |=  *)
 
 PWrap has primitive projections with eta conversion.
@@ -12,7 +13,8 @@ fun (A : Type@{uu}) (p : PWrap@{uu} A) => punwrap _ p
 (* uu |=  *)
 
 Arguments punwrap _%type_scope _
-Record RWrap (A : Type@{uu}) : Type@{uu} := rwrap { runwrap : A }
+Record RWrap (A : Type@{uu}) : Type@{uu} := rwrap
+  { runwrap : A }.
 (* uu |=  *)
 
 Arguments RWrap _%type_scope
@@ -80,9 +82,9 @@ foo@{uu u v} =
 Type@{u} -> Type@{v} -> Type@{uu}
      : Type@{max(uu+1,u+1,v+1)}
 (* uu u v |=  *)
-Inductive Empty@{E} : Type@{E} :=  
+Inductive Empty@{E} : Type@{E} :=  .
 (* E |=  *)
-Record PWrap (A : Type@{E}) : Type@{E} := pwrap { punwrap : A }
+Record PWrap (A : Type@{E}) : Type@{E} := pwrap { punwrap : A }.
 (* E |=  *)
 
 PWrap has primitive projections with eta conversion.
@@ -107,7 +109,7 @@ insec@{v} = Type@{uu} -> Type@{v}
      : Type@{max(uu+1,v+1)}
 (* v |=  *)
 Inductive insecind@{k} : Type@{k+1} :=
-    inseccstr : Type@{k} -> insecind@{k}
+    inseccstr : Type@{k} -> insecind@{k}.
 (* k |=  *)
 
 Arguments inseccstr _%type_scope
@@ -115,7 +117,7 @@ insec@{uu v} = Type@{uu} -> Type@{v}
      : Type@{max(uu+1,v+1)}
 (* uu v |=  *)
 Inductive insecind@{uu k} : Type@{k+1} :=
-    inseccstr : Type@{k} -> insecind@{uu k}
+    inseccstr : Type@{k} -> insecind@{uu k}.
 (* uu k |=  *)
 
 Arguments inseccstr _%type_scope
@@ -162,6 +164,9 @@ When declaring multiple axioms in one command, only the first is allowed a unive
 foo@{i} = Type@{M.i} -> Type@{i}
      : Type@{max(M.i+1,i+1)}
 (* i |=  *)
+Type@{u0} -> Type@{UnivBinders.64}
+     : Type@{max(u0+1,UnivBinders.64+1)}
+(* {UnivBinders.64} |=  *)
 bind_univs.mono = 
 Type@{bind_univs.mono.u}
      : Type@{bind_univs.mono.u+1}
diff --git a/test-suite/output/UnivBinders.v b/test-suite/output/UnivBinders.v
index ed6e90b2a6..9539e34cfe 100644
--- a/test-suite/output/UnivBinders.v
+++ b/test-suite/output/UnivBinders.v
@@ -161,6 +161,16 @@ Module Notas.
 
 End Notas.
 
+Module NoAutoNames.
+  Monomorphic Universe u0.
+
+  (* The anonymous universe doesn't get a name (names are only
+     invented at the end of a definition/inductive) so no need to
+     qualify u0. *)
+  Check (Type@{u0} -> Type).
+
+End NoAutoNames.
+
 (* Universe binders survive through compilation, sections and modules. *)
 Require TestSuite.bind_univs.
 Print bind_univs.mono.
diff --git a/test-suite/output/bug_12908.v b/test-suite/output/bug_12908.v
index 6f7be22fa0..7ab218a27a 100644
--- a/test-suite/output/bug_12908.v
+++ b/test-suite/output/bug_12908.v
@@ -7,7 +7,7 @@ Check forall m n, mult' m n = Nat.mul (Nat.mul 2 m) n.
 End A.
 
 Module B.
-(* Test that an overriden scoped notation is deactivated *)
+(* Test that an overridden scoped notation is deactivated *)
 Infix "*" := mult' : nat_scope.
 Check forall m n, mult' m n = Nat.mul (Nat.mul 2 m) n.
 End B.
diff --git a/test-suite/output/bug_13595.out b/test-suite/output/bug_13595.out
new file mode 100644
index 0000000000..2423b77b55
--- /dev/null
+++ b/test-suite/output/bug_13595.out
@@ -0,0 +1,4 @@
+The command has indeed failed with message:
+Tactic failure: Goal is solvable by congruence but some arguments are missing.
+  Try "congruence with ((Triple a _ _)) ((Triple d c _))",
+  replacing metavariables by arbitrary terms.
diff --git a/test-suite/output/bug_13595.v b/test-suite/output/bug_13595.v
new file mode 100644
index 0000000000..27a9ebe15d
--- /dev/null
+++ b/test-suite/output/bug_13595.v
@@ -0,0 +1,8 @@
+Inductive Cube:Set :=| Triple: nat -> nat -> nat -> Cube.
+
+Theorem incomplete :forall a b c d : nat,Triple a = Triple b->Triple d c = Triple d b->a = c.
+Proof.
+  Fail congruence.
+  intros.
+  congruence with ((Triple a a a)) ((Triple d c a)).
+Qed.
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/test-suite/primitive/uint63/addcarryc.v b/test-suite/primitive/uint63/addcarryc.v
index a4430769ca..7ab3af51d8 100644
--- a/test-suite/primitive/uint63/addcarryc.v
+++ b/test-suite/primitive/uint63/addcarryc.v
@@ -1,4 +1,4 @@
-Require Import Int63.
+Require Import PrimInt63.
 
 Set Implicit Arguments.
 
diff --git a/test-suite/primitive/uint63/addmuldiv.v b/test-suite/primitive/uint63/addmuldiv.v
index 72b0164b49..e3aded6c96 100644
--- a/test-suite/primitive/uint63/addmuldiv.v
+++ b/test-suite/primitive/uint63/addmuldiv.v
@@ -1,4 +1,4 @@
-Require Import Int63.
+Require Import PrimInt63.
 
 Set Implicit Arguments.
 
diff --git a/test-suite/primitive/uint63/diveucl.v b/test-suite/primitive/uint63/diveucl.v
index 8f88a0f356..43a0741ffe 100644
--- a/test-suite/primitive/uint63/diveucl.v
+++ b/test-suite/primitive/uint63/diveucl.v
@@ -1,4 +1,4 @@
-Require Import Int63.
+Require Import PrimInt63.
 
 Set Implicit Arguments.
 
diff --git a/test-suite/primitive/uint63/head0.v b/test-suite/primitive/uint63/head0.v
index f4234d2605..30cbce4537 100644
--- a/test-suite/primitive/uint63/head0.v
+++ b/test-suite/primitive/uint63/head0.v
@@ -1,4 +1,4 @@
-Require Import Int63.
+Require Import PrimInt63.
 
 Set Implicit Arguments.
 
diff --git a/test-suite/primitive/uint63/subcarryc.v b/test-suite/primitive/uint63/subcarryc.v
index e81b6536b2..6a773dde5d 100644
--- a/test-suite/primitive/uint63/subcarryc.v
+++ b/test-suite/primitive/uint63/subcarryc.v
@@ -1,4 +1,4 @@
-Require Import Int63.
+Require Import PrimInt63.
 
 Set Implicit Arguments.
 
diff --git a/test-suite/primitive/uint63/tail0.v b/test-suite/primitive/uint63/tail0.v
index c9d426087a..1f91e4106c 100644
--- a/test-suite/primitive/uint63/tail0.v
+++ b/test-suite/primitive/uint63/tail0.v
@@ -1,4 +1,4 @@
-Require Import Int63.
+Require Import PrimInt63.
 
 Set Implicit Arguments.
 
diff --git a/test-suite/success/Case22.v b/test-suite/success/Case22.v
index 465b3eb8c0..90c1b308f2 100644
--- a/test-suite/success/Case22.v
+++ b/test-suite/success/Case22.v
@@ -89,3 +89,16 @@ Check fun x:Ind bool nat =>
   match x in Ind _ X Y Z return Z with
   | y => (true,0)
   end.
+
+(* A check that multi-implicit arguments work *)
+
+Check fun x : {True}+{False} => match x with left _ _ => 0 | right _ _ => 1 end.
+Check fun x : {True}+{False} => match x with left _ => 0 | right _ => 1 end.
+
+(* Check that Asymmetric Patterns does not apply to the in clause *)
+
+Inductive expr {A} : A -> Type := intro : forall {n:nat} (a:A), n=n -> expr a.
+Check fun (x:expr true) => match x in expr n return n=n with intro _ _ => eq_refl end.
+Set Asymmetric Patterns.
+Check fun (x:expr true) => match x in expr n return n=n with intro _ a _ => eq_refl a end.
+Unset Asymmetric Patterns.
diff --git a/test-suite/success/Cases.v b/test-suite/success/Cases.v
index 232ac17cbf..e678fc7882 100644
--- a/test-suite/success/Cases.v
+++ b/test-suite/success/Cases.v
@@ -1882,3 +1882,60 @@ Check match O in nat return nat with O => O | _ => O end.
 (* Checking that aliases are substituted in the correct order *)
 
 Check match eq_refl (1,0) in _ = (y as z, y' as z) return z = z with eq_refl => eq_refl end : 0=0.
+
+(* Checking use of argument scopes *)
+
+Module Intern.
+
+Inductive I (A:Type) := C : nat -> let a:=0 in bool -> list bool -> bool -> I A.
+
+Close Scope nat_scope.
+Notation "0" := true : bool_scope.
+Notation "0" := nil : list_scope.
+Notation C' := @C (only parsing).
+Notation C'' := C (only parsing).
+Notation C''' := (C _ 0) (only parsing).
+
+Set Asymmetric Patterns.
+
+Check fun x => match x with C 0 0 0 0 => O | _ => O end. (* 8.5 regression *)
+Check fun x => match x with C 0 _ 0 0 0 => O | _ => O end. (* was not supported *)
+
+Check fun x => match x with C' 0 0 0 0 => O | _ => O end. (* 8.5 regression *)
+Check fun x => match x with C' _ 0 0 0 => O | _ => O end. (* 8.5 regression *)
+Check fun x => match x with C' 0 _ 0 0 0 => O | _ => O end. (* was not supported *)
+Check fun x => match x with C' _ _ 0 0 0 => O | _ => O end. (* was pre 8.5 bug *)
+
+Check fun x => match x with C'' 0 0 0 0 => O | _ => O end. (* 8.5 regression *)
+Check fun x => match x with C'' _ 0 0 0 => O | _ => O end. (* 8.5 regression *)
+Check fun x => match x with C'' 0 _ 0 0 0 => O | _ => O end. (* was not supported *)
+Check fun x => match x with C'' _ _ 0 0 0 => O | _ => O end. (* was pre 8.5 bug *)
+
+Check fun x => match x with C''' 0 0 0 => O | _ => O end. (* 8.5 regression *)
+Check fun x => match x with C''' _ 0 0 0 => O | _ => O end. (* was not supported  *)
+
+Unset Asymmetric Patterns.
+Arguments C {A} _ {x} _ _.
+
+Check fun x => match x with C 0 0 0 => O | _ => O end. (* was ok *)
+Check fun x => match x with C 0 _ 0 0 => O | _ => O end. (* was wrong scope on last argument with let-in *)
+
+Check fun x => match x with C' _ 0 _ 0 0 => O | _ => O end. (* was wrong scope *)
+Check fun x => match x with C' _ 0 _ 0 0 0 => O | _ => O end. (* was wrong scope *)
+
+Check fun x => match x with C'' _ 0 0 => O | _ => O end. (* was ok *)
+Check fun x => match x with C'' _ _ 0 0 => O | _ => O end. (* was wrong scope *)
+
+Check fun x => match x with C''' 0 0 => O | _ => O end. (* was wrong scope *)
+Check fun x => match x with C''' _ 0 0 => O | _ => O end. (* works by miscount compensating *)
+
+Check fun x => match x with (@C _ 0) _ 0 0 => O | _ => O end. (* was wrong scope *)
+Check fun x => match x with (@C _ 0) _ _ 0 0 => O | _ => O end. (* was wrong scope *)
+
+Check fun x => match x with @C _ 0 _ 0 0 => O | _ => O end. (* was ok *)
+Check fun x => match x with @C _ 0 _ _ 0 0 => O | _ => O end. (* was wrong scope *)
+
+Check fun x => match x with (@C) _ O _ 0 0 => O | _ => O end. (* was wrong scope *)
+Check fun x => match x with (@C) _ O _ _ 0 0 => O | _ => O end. (* was wrong scope *)
+
+End Intern.
diff --git a/test-suite/success/autorewrite.v b/test-suite/success/autorewrite.v
index 71d333d439..0ac62fcdc9 100644
--- a/test-suite/success/autorewrite.v
+++ b/test-suite/success/autorewrite.v
@@ -4,25 +4,35 @@ Axiom Ack0 : forall m : nat, Ack 0 m = S m.
 Axiom Ack1 : forall n : nat, Ack (S n) 0 = Ack n 1.
 Axiom Ack2 : forall n m : nat, Ack (S n) (S m) = Ack n (Ack (S n) m).
 
-Hint Rewrite Ack0 Ack1 Ack2 : base0.
+Module M.
+  #[export] Hint Rewrite Ack0 Ack1 Ack2 : base0.
 
-Lemma ResAck0 : (Ack 2 2 = 7 -> False) -> False.
+  Lemma ResAck0 : (Ack 2 2 = 7 -> False) -> False.
+  Proof.
+    intros.
+    autorewrite with base0 in H using try (apply H; reflexivity).
+  Qed.
+End M.
+
+Lemma ResAck1 : forall H:(Ack 2 2 = 7 -> False), True -> False.
 Proof.
   intros.
-  autorewrite with base0 in H using try (apply H; reflexivity).
-Qed.
+  Fail autorewrite with base0 in *.
+Abort.
+
+Import M.
 
 Lemma ResAck1 : forall H:(Ack 2 2 = 7 -> False), True -> False.
 Proof.
   intros.
   autorewrite with base0 in *.
-    apply H;reflexivity.
+ apply H;reflexivity.
 Qed.
 
 (* Check autorewrite does not solve existing evars *)
 (* See discussion started by A. Chargueraud in Oct 2010 on coqdev *)
 
-Hint Rewrite <- plus_n_O : base1.
+Global Hint Rewrite <- plus_n_O : base1.
 Goal forall y, exists x, y+x = y.
 eexists. autorewrite with base1.
 Fail reflexivity.
diff --git a/test-suite/success/case_let_conversion.v b/test-suite/success/case_let_conversion.v
new file mode 100644
index 0000000000..3f1ab96fe1
--- /dev/null
+++ b/test-suite/success/case_let_conversion.v
@@ -0,0 +1,39 @@
+Axiom checker_flags : Set.
+
+Inductive Box (R : Type) : Type := box : Box R.
+
+Inductive typing (H : checker_flags) : Type :=
+| type_Rel : typing H -> typing H
+| type_Case : let i := tt in Box (typing H) -> typing H.
+
+Definition unbox (P : Type) (b : Box P) := match b with box _ => 0 end.
+
+Definition size (H : checker_flags) (d : typing H) : nat.
+Proof.
+revert d.
+fix size 1.
+destruct 1.
+- exact (size d).
+- exact (unbox _ b).
+Defined.
+
+Definition foo (H : checker_flags) (a : typing H) :
+  size H (type_Rel H a) = size H a.
+Proof.
+simpl.
+reflexivity.
+Qed.
+
+Definition bar (H : checker_flags) (a : typing H) :
+  size H (type_Rel H a) = size H a.
+Proof.
+vm_compute.
+reflexivity.
+Qed.
+
+Definition qux (H : checker_flags) (a : typing H) :
+  size H (type_Rel H a) = size H a.
+Proof.
+native_compute.
+reflexivity.
+Qed.
diff --git a/test-suite/success/case_let_param.v b/test-suite/success/case_let_param.v
new file mode 100644
index 0000000000..46d8c26e83
--- /dev/null
+++ b/test-suite/success/case_let_param.v
@@ -0,0 +1,15 @@
+Inductive foo (x := tt) := Foo : forall (y := x), foo.
+
+Definition get (t : foo) := match t with Foo _ y => y end.
+
+Goal get Foo = tt.
+Proof.
+reflexivity.
+Qed.
+
+Goal forall x : foo,
+  match x with Foo _ y => y end = match x with Foo _ _ => tt end.
+Proof.
+intros.
+reflexivity.
+Qed.
diff --git a/test-suite/success/cbv_let.v b/test-suite/success/cbv_let.v
new file mode 100644
index 0000000000..861a73a64e
--- /dev/null
+++ b/test-suite/success/cbv_let.v
@@ -0,0 +1,34 @@
+Record T : Type := Build_T { f : unit; g := pair f f; }.
+
+Definition t : T := {| f := tt; |}.
+
+Goal match t return unit with Build_T f g => f end = tt.
+Proof.
+cbv.
+reflexivity.
+Qed.
+
+Goal match t return prod unit unit with Build_T f g => g end = pair tt tt.
+Proof.
+cbv.
+reflexivity.
+Qed.
+
+Goal forall (x : T),
+  match x return prod unit unit with Build_T f g => g end =
+  pair match x return unit with Build_T f g => fst g end match x return unit with Build_T f g => snd g end.
+Proof.
+cbv.
+destruct x.
+reflexivity.
+Qed.
+
+Record U : Type := Build_U { h := tt }.
+
+Definition u : U := Build_U.
+
+Goal match u with Build_U h => h end = tt.
+Proof.
+cbv.
+reflexivity.
+Qed.
diff --git a/test-suite/success/change.v b/test-suite/success/change.v
index 2f676cf9ad..053429a5a9 100644
--- a/test-suite/success/change.v
+++ b/test-suite/success/change.v
@@ -14,8 +14,8 @@ Abort.
 (* Check the combination of at, with and in (see bug #2146) *)
 
 Goal 3=3 -> 3=3. intro H.
-change 3 at 2 with (1+2).
-change 3 at 2 with (1+2) in H |-.
+change 3 with (1+2) at 2.
+change 3 with (1+2) in H at 2 |-.
 change 3 with (1+2) in H at 1 |- * at 1.
 (* Now check that there are no more 3's *)
 change 3 with (1+2) in * || reflexivity.
diff --git a/test-suite/success/change_case.v b/test-suite/success/change_case.v
new file mode 100644
index 0000000000..490e4f4b6c
--- /dev/null
+++ b/test-suite/success/change_case.v
@@ -0,0 +1,20 @@
+Inductive box (A : Type) := Box : A -> box A.
+
+Axiom PRED : unit -> Prop.
+Axiom FUN : forall (u : unit), box (PRED u).
+
+Axiom U : unit.
+Definition V := U.
+
+Goal match FUN U with Box _ _ => True end.
+Proof.
+repeat match goal with
+| [ |- context G[ U ] ] =>
+ let e := context G [ V ] in
+ change e
+end.
+set (Z := V).
+clearbody Z. (* This fails if change misses the case parameters *)
+destruct (FUN Z).
+constructor.
+Qed.
diff --git a/test-suite/success/forward.v b/test-suite/success/forward.v
index 4e36dec15b..62c788e910 100644
--- a/test-suite/success/forward.v
+++ b/test-suite/success/forward.v
@@ -27,3 +27,7 @@ Fail match goal with |- (?f ?a) => idtac end. (* should be beta-iota reduced *)
 2:match goal with _: (?f ?a) |- _ => idtac end. (* should not be beta-iota reduced *)
 Abort.
 
+Goal nat.
+assert nat as J%S by exact 0.
+exact J.
+Qed.
diff --git a/test-suite/success/induct.v b/test-suite/success/induct.v
index 4983ee3c0d..615350c58c 100644
--- a/test-suite/success/induct.v
+++ b/test-suite/success/induct.v
@@ -154,50 +154,6 @@ induction H.
 change (0 = z -> True) in IHrepr''.
 Abort.
 
-(* Test double induction *)
-
-(* This was failing in 8.5 and before because of a bug in the order of
-   hypotheses *)
-
-Set Warnings "-deprecated".
-
-Inductive I2 : Type :=
-  C2 : forall x:nat, x=x -> I2.
-Goal forall a b:I2, a = b.
-double induction a b.
-Abort.
-
-(* This was leaving useless hypotheses in 8.5 and before because of
-   the same bug. This is a change of compatibility. *)
-
-Inductive I3 : Prop :=
-  C3 : forall x:nat, x=x -> I3.
-Goal forall a b:I3, a = b.
-double induction a b.
-Fail clear H. (* H should have been erased *)
-Abort.
-
-(* This one had quantification in reverse order in 8.5 and before *)
-(* This is a change of compatibility. *)
-
-Goal forall m n, le m n -> le n m -> n=m.
-intros m n. double induction 1 2.
-3:destruct 1. (* Should be "S m0 <= m0" *)
-Abort.
-
-(* Idem *)
-
-Goal forall m n p q, le m n -> le p q -> n+p=m+q.
-intros *. double induction 1 2.
-3:clear H2. (* H2 should have been erased *)
-Abort.
-
-(* This is unchanged *)
-
-Goal forall m n:nat, n=m.
-double induction m n.
-Abort.
-
 (* Mentioned as part of bug #12944 *)
 
 Inductive test : Set := cons : forall (IHv : nat) (v : test), test.
diff --git a/test-suite/success/intros.v b/test-suite/success/intros.v
index d37ad9f528..b8fbff05c6 100644
--- a/test-suite/success/intros.v
+++ b/test-suite/success/intros.v
@@ -152,3 +152,15 @@ Definition d := ltac:(intro x; exact (x*x)).
 Definition d' : nat -> _ := ltac:(intros;exact 0).
 
 End Evar.
+
+Module Wildcard.
+
+(* We check that the wildcard internal name does not interfere with
+   user fresh names (currently the prefix is "_H") *)
+
+Goal nat -> bool -> nat -> bool.
+intros _ ?_H ?_H.
+exact _H.
+Qed.
+
+End Wildcard.
diff --git a/test-suite/success/let_pattern_mismatch.v b/test-suite/success/let_pattern_mismatch.v
new file mode 100644
index 0000000000..a56a8fff4f
--- /dev/null
+++ b/test-suite/success/let_pattern_mismatch.v
@@ -0,0 +1,18 @@
+(* Weird corner case accepted by the pattern-matching algorithm. Destructuring
+   let-bindings in patterns can actually be shorter than the case they match. *)
+
+Inductive ascii : Set :=
+| Ascii : bool -> bool -> bool -> bool -> bool -> bool -> bool -> bool -> ascii.
+
+Definition dummy (a : ascii) : unit :=
+  let (a0,a1,a2,a3,a4,a5,a6,a7) := a in tt.
+
+Goal forall (a : ascii) (H : tt = dummy a), True.
+Proof.
+intros a H.
+unfold dummy in *.
+(* Two bound variables in the pattern, eight in the term. *)
+match goal with
+| H:context [ let (x, y) := ?X in _ ] |- _ => destruct X eqn:?
+end.
+Abort.
diff --git a/test-suite/success/match_case_pattern_variables.v b/test-suite/success/match_case_pattern_variables.v
new file mode 100644
index 0000000000..bb9117d033
--- /dev/null
+++ b/test-suite/success/match_case_pattern_variables.v
@@ -0,0 +1,34 @@
+(** Check that bound variables in case patterns are handled correctly. *)
+
+Goal forall (ch : unit) (t : list unit) (s : list unit),
+  match s with
+  | nil => False
+  | cons a l => ch = a /\ l = t
+  end.
+Proof.
+intros.
+match goal with
+| |- match ?e with
+    | nil => ?N
+    | cons a b => ?P
+    end =>
+     let f :=
+      constr:((fun (e' : list unit) => match e' with
+                          | nil => N
+                          | cons a b => P
+                          end))
+     in
+     change (f e)
+end.
+Abort.
+
+Goal forall (ch : unit) (n : nat) (s : prod unit nat),
+  let (a, l) := s in ch = a /\ l = n.
+Proof.
+intros.
+match goal with
+| [ |- let (a, b) := ?e in ?P ] =>
+  let f := constr:((fun (e' : prod unit nat) => match e' with pair a b => P end)) in
+  change (f e)
+end.
+Abort.
diff --git a/test-suite/success/rewrite_in.v b/test-suite/success/rewrite_in.v
index 29fe915ff4..3433866239 100644
--- a/test-suite/success/rewrite_in.v
+++ b/test-suite/success/rewrite_in.v
@@ -5,4 +5,10 @@ Goal forall (P Q : Prop) (f:P->Prop) (p:P), (P<->Q) -> f p -> True.
   rewrite H in p || trivial.
 Qed.
 
-
+Goal 1 = 0 -> 0 = 1.
+  intro H.
+  Fail rewrite H at 1 2 3. (* bug #13566 *)
+  Fail rewrite H at 0.
+  rewrite H at 1.
+  reflexivity.
+Qed.