97 files changed, 1404 insertions, 276 deletions

diff --git a/test-suite/Makefile b/test-suite/Makefile
index 245c717d42..2a2f62e23f 100644
--- a/test-suite/Makefile
+++ b/test-suite/Makefile
@@ -46,7 +46,11 @@ BIN := $(ROOT)/bin/
 
 COQLIB?=
 ifeq ($(COQLIB),)
+ ifeq ($(LOCAL),true)
   COQLIB := $(shell ocaml ocaml_pwd.ml ..)
+ else
+  COQLIB := $(shell ocaml ocaml_pwd.ml $(COQLIBINSTALL))
+ endif
 endif
 endif # exists ../_build
 export COQLIB
@@ -320,7 +324,7 @@ unit-tests: $(UNIT_LOGFILES)
 # Build executable, run it to generate log file
 unit-tests/%.ml.log: unit-tests/%.ml unit-tests/src/$(UNIT_LINK)
 	$(SHOW) 'TEST      $<'
-	$(HIDE)$(OCAMLBEST) -linkall -linkpkg -package coq.toplevel,ounit2 \
+	$(HIDE)$(OCAMLBEST) -linkall -linkpkg -package coq-core.toplevel,ounit2 \
 	     -I unit-tests/src $(UNIT_LINK) $< -o $<.test;
 	$(HIDE)./$<.test
 
diff --git a/test-suite/bugs/closed/bug_12011.v b/test-suite/bugs/closed/bug_12011.v
new file mode 100644
index 0000000000..f149b4e8ae
--- /dev/null
+++ b/test-suite/bugs/closed/bug_12011.v
@@ -0,0 +1,21 @@
+From Coq Require Import Setoid ssreflect.
+
+Lemma test A (R : relation A) `{Equivalence _ R} (x y z : A) :
+  R x y -> R y z -> R x z.
+Proof.
+  intros Hxy Hyz.
+  rewrite -Hxy in Hyz.
+  exact Hyz.
+Qed.
+
+
+
+Axiom envs_lookup_delete : bool.
+Axiom envs_lookup_delete_Some : envs_lookup_delete = true <-> False.
+
+Goal envs_lookup_delete = true -> False.
+Proof.
+intros Hlookup.
+rewrite envs_lookup_delete_Some in Hlookup *. (* <- used to revert Hlookup *)
+exact Hlookup.
+Qed.
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_13586.v b/test-suite/bugs/closed/bug_13586.v
new file mode 100644
index 0000000000..6a739c364a
--- /dev/null
+++ b/test-suite/bugs/closed/bug_13586.v
@@ -0,0 +1,6 @@
+Goal True.
+Fail timeout 2 ((timeout 1 repeat cut True) || (repeat cut True)).
+Fail Timeout 2 ((timeout 1 repeat cut True) || (repeat cut True)).
+Fail timeout 1 ((timeout 2 repeat cut True) || idtac "fail").
+auto.
+Qed.
diff --git a/test-suite/bugs/closed/bug_13732.v b/test-suite/bugs/closed/bug_13732.v
new file mode 100644
index 0000000000..24840abdf6
--- /dev/null
+++ b/test-suite/bugs/closed/bug_13732.v
@@ -0,0 +1,16 @@
+Module Sort.
+  Set Printing Universes.
+
+  Implicit Types TT : Type.
+
+  Check fun TT => nat.
+End Sort.
+
+Module Ref.
+  Set Universe Polymorphism.
+
+  Axiom tele : Type.
+
+  Implicit Types TT : tele.
+  Check fun TT => nat.
+End Ref.
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/closed/bug_13841.v b/test-suite/bugs/closed/bug_13841.v
new file mode 100644
index 0000000000..60fca8b49c
--- /dev/null
+++ b/test-suite/bugs/closed/bug_13841.v
@@ -0,0 +1,11 @@
+Goal True.
+evar (p : bool).
+unify ?p true.
+let v := eval vm_compute in (orb p false) in
+match v with true => idtac end.
+assert (orb p false = true).
+vm_compute.
+match goal with |- true = _ => idtac end.
+easy.
+easy.
+Qed.
diff --git a/test-suite/bugs/closed/bug_13896.v b/test-suite/bugs/closed/bug_13896.v
new file mode 100644
index 0000000000..10f24d8564
--- /dev/null
+++ b/test-suite/bugs/closed/bug_13896.v
@@ -0,0 +1,24 @@
+Inductive type : Set :=
+    Tptr : type -> type
+  | Tref : type -> type
+  | Trv_ref : type -> type
+  | Tint : type -> type -> type
+  | Tvoid : type
+  | Tarray : type -> type -> type
+  | Tnamed : type -> type
+  | Tfunction : type -> type -> type -> type
+  | Tbool : type
+  | Tmember_pointer : type -> type -> type
+  | Tfloat : type -> type
+  | Tqualified : type -> type -> type
+  | Tnullptr : type
+  | Tarch : type -> type -> type
+.
+Definition type_eq_dec : forall (ty1 ty2 : type), { ty1 = ty2 } + { ty1 <> ty2 }.
+Proof. fix IHty1 1.  decide equality. Defined.
+
+Goal (if type_eq_dec (Tptr Tvoid) (Tptr Tvoid) then True else False).
+Proof.
+timeout 1 cbn.
+constructor.
+Qed.
diff --git a/test-suite/bugs/closed/bug_4836.v b/test-suite/bugs/closed/bug_4836.v
index 9aefb10172..62d39619b0 100644
--- a/test-suite/bugs/closed/bug_4836.v
+++ b/test-suite/bugs/closed/bug_4836.v
@@ -1 +1 @@
-(* -*- coq-prog-args: ("bugs/closed/PLACEHOLDER.v") -*- *)
+(* Placeholder file for directory / file test *)
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/bugs/closed/bug_7631.v b/test-suite/bugs/closed/bug_7631.v
index 93aeb83e28..14ab4de9b7 100644
--- a/test-suite/bugs/closed/bug_7631.v
+++ b/test-suite/bugs/closed/bug_7631.v
@@ -21,3 +21,9 @@ Definition bar (x := foo) := Eval native_compute in x.
 Definition barvm (x := foo) := Eval vm_compute in x.
 
 End RelContext.
+
+Definition bar (t:=_) (x := true : t) := Eval native_compute in x.
+Definition barvm (t:=_) (x := true : t) := Eval vm_compute in x.
+
+Definition baz (z:nat) (t:=_ z) (x := true : t) := Eval native_compute in x.
+Definition bazvm (z:nat) (t:=_ z) (x := true : t) := Eval vm_compute in x.
diff --git a/test-suite/coq-makefile/timing/precomputed-time-tests/007-no-output-sync/time-of-build.log.in b/test-suite/coq-makefile/timing/precomputed-time-tests/007-no-output-sync/time-of-build.log.in
index 47d0e09e1a..258eb04271 100644
--- a/test-suite/coq-makefile/timing/precomputed-time-tests/007-no-output-sync/time-of-build.log.in
+++ b/test-suite/coq-makefile/timing/precomputed-time-tests/007-no-output-sync/time-of-build.log.in
@@ -744,7 +744,7 @@ CONTRIBUTING.md
 CREDITS
 INSTALL.md
 LICENSE
-META.coq.in
+META.coq-core.in
 Makefile
 Makefile.build
 Makefile.checker
@@ -5626,4 +5626,4 @@ ValueError: too many values to unpack
 Makefile.ci:90: recipe for target 'ci-metacoq' failed
 make: *** [ci-metacoq] Error 1
 section_end:1598965182:build_script
section_start:1598965182:after_script
section_end:1598965184:after_script
section_start:1598965184:upload_artifacts_on_failure
section_end:1598965189:upload_artifacts_on_failure
ERROR: Job failed: exit code 1
-
\ No newline at end of file
+
diff --git a/test-suite/dune b/test-suite/dune
index 1864153021..09597fc864 100644
--- a/test-suite/dune
+++ b/test-suite/dune
@@ -35,7 +35,8 @@
    ; For the changelog test
    ../config/coq_config.py
    (source_tree doc/changelog)
-   (package coq)
+   (package coq-core)
+   (package coq-stdlib)
    ; For fake_ide
    (package coqide-server)
    (source_tree .))
diff --git a/test-suite/ltac2/ind.v b/test-suite/ltac2/ind.v
new file mode 100644
index 0000000000..6f7352d224
--- /dev/null
+++ b/test-suite/ltac2/ind.v
@@ -0,0 +1,25 @@
+Require Import Ltac2.Ltac2.
+Require Import Ltac2.Option.
+
+Ltac2 Eval
+  let nat := Option.get (Env.get [@Coq; @Init; @Datatypes; @nat]) in
+  let nat := match nat with
+  | Std.IndRef nat => nat
+  | _ => Control.throw Not_found
+  end in
+  let data := Ind.data nat in
+  (* Check that there is only one inductive in the block *)
+  let ntypes := Ind.nblocks data in
+  let () := if Int.equal ntypes 1 then () else Control.throw Not_found in
+  let nat' := Ind.repr (Ind.get_block data 0) in
+  (* Check it corresponds *)
+  let () := if Ind.equal nat nat' then () else Control.throw Not_found in
+  let () := if Int.equal (Ind.index nat) 0 then () else Control.throw Not_found in
+  (* Check the number of constructors *)
+  let nconstr := Ind.nconstructors data in
+  let () := if Int.equal nconstr 2 then () else Control.throw Not_found in
+  (* Create a fresh instance *)
+  let s := Ind.get_constructor data 1 in
+  let s := Env.instantiate (Std.ConstructRef s) in
+  constr:($s 0)
+.
diff --git a/test-suite/ltac2/printf.v b/test-suite/ltac2/printf.v
new file mode 100644
index 0000000000..f96a01a9c9
--- /dev/null
+++ b/test-suite/ltac2/printf.v
@@ -0,0 +1,31 @@
+Require Import Ltac2.Ltac2.
+Require Import Ltac2.Printf.
+
+(* Check that the arguments have type unit *)
+Ltac2 ignore (x : unit) := ().
+
+Ltac2 dummy (_ : unit) (_ : int) := Message.of_string "dummy".
+
+(** Simple test for all specifications *)
+
+Ltac2 Eval ignore (printf "%i" 42).
+Ltac2 Eval ignore (printf "%s" "abc").
+Ltac2 Eval ignore (printf "%I" @Foo).
+Ltac2 Eval ignore (printf "%t" '(1 + 1 = 0)).
+Ltac2 Eval ignore (printf "%%").
+Ltac2 Eval ignore (printf "%a" dummy 18).
+
+(** More complex tests *)
+
+Ltac2 Eval ignore (printf "%I foo%a bar %s" @ok dummy 18 "yes").
+
+Ltac2 Eval Message.print (fprintf "%I foo%a bar %s" @ok dummy 18 "yes").
+
+(** Failure tests *)
+
+Fail Ltac2 Eval printf "%i" "foo".
+Fail Ltac2 Eval printf "%s" 0.
+Fail Ltac2 Eval printf "%I" "foo".
+Fail Ltac2 Eval printf "%t" "foo".
+Fail Ltac2 Eval printf "%a" (fun _ _ => ()).
+Fail Ltac2 Eval printf "%a" (fun _ i => Message.of_int i) "foo".
diff --git a/test-suite/micromega/bug_13794.v b/test-suite/micromega/bug_13794.v
new file mode 100644
index 0000000000..5e303a0b7f
--- /dev/null
+++ b/test-suite/micromega/bug_13794.v
@@ -0,0 +1,39 @@
+From Coq Require Import Lia ZArith.ZArith NArith.NArith.
+Unset Nia Cache.
+
+Open Scope N_scope.
+
+
+Lemma over (n0 n1 n2 n3 n4 n5 n6 : N)
+  (e0 : 1 + 8 * n0 = n1 * n1 + n2)
+  (e1 : n1 - 1 = 2 * n3 + n4)
+  (e2 : n3 * (1 + n3) = 2 * n5)
+  (e3 : n2 + 2 * n4 * n1 - n4 = 8 * n6)
+  (o0 : n4 = 0 \/ n4 = 1) :
+  n6 = n0 - n5.
+Proof.
+  Time nia.
+Qed.
+
+Lemma over2 (n0 n1 n2 n3 n4 n5 n6 : N)
+  (e0 : 1 + 8 * n0 = n1 * n1 + n2)
+  (e1 : n1 + 1 = 2 * n3 + n4)
+  (e2 : n3 * (1 + n3) = 2 * n5)
+  (e3 : n2 + 2 * n4 * n1 + n4 = 8 * n6)
+  (o0 : n4 = 0) :
+  n6 = n0 + n5.
+Proof.
+  Fail nia.
+Abort.
+
+Open Scope Z_scope.
+
+Lemma over3 (n1 n2 n3 n4 n5 : Z)
+  (e : 0 <= n1 /\ 0 <= n2 /\ 0 <= n3 /\ 0 <= n4
+   /\ 0 <= n5)
+  (e1 : n1 + 1 = 20 * n3 + n4)
+  (e3 : n2 + 2 * n4 * n1 + n4 = 8 * n5) :
+  n5 = 0.
+Proof.
+Time Fail nia.
+Abort.
diff --git a/test-suite/misc/coq_environment.sh b/test-suite/misc/coq_environment.sh
index 667d11f89e..6f7b11c8f1 100755
--- a/test-suite/misc/coq_environment.sh
+++ b/test-suite/misc/coq_environment.sh
@@ -16,7 +16,7 @@ EOT
 cp $BIN/coqc .
 cp $BIN/coq_makefile .
 mkdir -p overridden/tools/
-cp $COQLIB/tools/CoqMakefile.in overridden/tools/
+cp $COQLIB/tools/CoqMakefile.in overridden/tools/ || cp $COQLIB/../coq-core/tools/CoqMakefile.in overridden/tools/
 
 unset COQLIB
 N=`./coqc -config | grep COQLIB | grep /overridden | wc -l`
diff --git a/test-suite/misc/coqtop_print-mod-uid.sh b/test-suite/misc/coqtop_print-mod-uid.sh
new file mode 100755
index 0000000000..db1df4bb4b
--- /dev/null
+++ b/test-suite/misc/coqtop_print-mod-uid.sh
@@ -0,0 +1,6 @@
+#!/usr/bin/env bash
+
+export COQBIN=$BIN
+export PATH=$COQBIN:$PATH
+
+[ "$(coqtop -print-mod-uid prerequisite/admit.vo)" = "prerequisite/.coq-native/NTestSuite_admit" ]
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/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 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/DebugFlags.out b/test-suite/output/DebugFlags.out
new file mode 100644
index 0000000000..0385413937
--- /dev/null
+++ b/test-suite/output/DebugFlags.out
@@ -0,0 +1,44 @@
+File "stdin", line 1, characters 0-16:
+Warning: There is no debug flag "cbn". [unknown-debug-flag,option]
+Debug: [RAKAM] <<forall A : Type, A -> A -> Prop|>>
+Debug: [RAKAM] <><><><><>
+Debug: [RAKAM] <<forall A : Type, A -> A -> Prop|>>
+Debug: [RAKAM] <><><><><>
+Debug: [RAKAM] <<?A -> ?A -> Prop|>>
+Debug: [RAKAM] <><><><><>
+Debug: [RAKAM] <<?A -> ?A -> Prop|>>
+Debug: [RAKAM] <><><><><>
+Debug: [RAKAM] <<nat -> nat -> nat|>>
+Debug: [RAKAM] <><><><><>
+Debug: [RAKAM] <<nat -> nat -> nat|>>
+Debug: [RAKAM] <><><><><>
+Debug: [RAKAM] <<nat -> nat|>>
+Debug: [RAKAM] <><><><><>
+Debug: [RAKAM] <<nat -> nat|>>
+Debug: [RAKAM] <><><><><>
+Debug: [RAKAM] <<nat -> nat|>>
+Debug: [RAKAM] <><><><><>
+Debug: [RAKAM] <<nat -> nat|>>
+Debug: [RAKAM] <><><><><>
+Debug: [RAKAM] <<nat -> nat|>>
+Debug: [RAKAM] <><><><><>
+Debug: [RAKAM] <<nat -> nat|>>
+Debug: [RAKAM] <><><><><>
+Debug: [RAKAM] <<nat -> nat|>>
+Debug: [RAKAM] <><><><><>
+Debug: [RAKAM] <<nat -> nat|>>
+Debug: [RAKAM] <><><><><>
+Debug: [RAKAM] <<nat -> nat|>>
+Debug: [RAKAM] <><><><><>
+Debug: [RAKAM] <<nat -> nat|>>
+Debug: [RAKAM] <><><><><>
+Debug: [RAKAM] <<nat -> nat|>>
+Debug: [RAKAM] <><><><><>
+Debug: [RAKAM] <<nat -> nat|>>
+Debug: [RAKAM] <><><><><>
+Debug: [RAKAM] <<nat -> Prop|>>
+Debug: [RAKAM] <><><><><>
+Debug: [RAKAM] <<nat -> Prop|>>
+Debug: [RAKAM] <><><><><>
+2 + 3 = 0
+     : Prop
diff --git a/test-suite/output/DebugFlags.v b/test-suite/output/DebugFlags.v
new file mode 100644
index 0000000000..32c0f2d24b
--- /dev/null
+++ b/test-suite/output/DebugFlags.v
@@ -0,0 +1,5 @@
+Set Debug "cbn".
+
+Set Debug "RAKAM".
+
+Check 2 + 3 = 0.
diff --git a/test-suite/bugs/closed/PLACEHOLDER.v b/test-suite/output/Function.out
index e69de29bb2..e69de29bb2 100644
--- a/test-suite/bugs/closed/PLACEHOLDER.v
+++ 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 ca8e1b58a8..96af456891 100644
--- a/test-suite/output/Int63Syntax.out
+++ b/test-suite/output/Int63Syntax.out
@@ -15,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.PrimInt63.int
+Cannot interpret this number as a value of type int
 The command has indeed failed with message:
-Cannot interpret this number as a value of type Coq.Numbers.Cyclic.Int63.PrimInt63.int
+Cannot interpret this number as a value of type int
 0
      : int
 0
@@ -33,9 +33,11 @@ The reference x was not found in the current environment.
 add 2 2
      : int
 The command has indeed failed with message:
-int63 are only non-negative numbers.
+Cannot interpret this number as a value of type int
 The command has indeed failed with message:
 overflow in int63 literal: 9223372036854775808
+0x1
+     : int
 2
      : nat
 2%int63
@@ -56,3 +58,21 @@ t = 2%i63
      : 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 6f1046f7a5..be0ee701af 100644
--- a/test-suite/output/Int63Syntax.v
+++ b/test-suite/output/Int63Syntax.v
@@ -20,6 +20,11 @@ Fail Check 0x.
 Check (PrimInt63.add 2 2).
 Fail Check -1.
 Fail Check 9223372036854775808.
+
+Set Printing All.
+Check 1%int63.
+Unset Printing All.
+
 Open Scope nat_scope.
 Check 2. (* : nat *)
 Check 2%int63.
@@ -40,3 +45,18 @@ 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..cc9e745f6b 100644
--- a/test-suite/output/Notations3.out
+++ b/test-suite/output/Notations3.out
@@ -6,7 +6,7 @@
      : nat * nat * (nat * nat)
 (0, 2, (2, 2))
      : nat * nat * (nat * nat)
-pair (pair O (S (S O))) (pair (S (S O)) O)
+pair (pair 0 2) (pair 2 0)
      : prod (prod nat nat) (prod nat nat)
 << 0, 2, 4 >>
      : nat * nat * nat * (nat * (nat * nat))
@@ -16,8 +16,7 @@ pair (pair O (S (S O))) (pair (S (S O)) O)
      : nat * nat * nat * (nat * (nat * nat))
 (0, 2, 4, (0, (2, 4)))
      : nat * nat * nat * (nat * (nat * nat))
-pair (pair (pair O (S (S O))) (S (S (S (S O)))))
-  (pair (S (S (S (S O)))) (pair (S (S O)) O))
+pair (pair (pair 0 2) 4) (pair 4 (pair 2 0))
      : prod (prod (prod nat nat) nat) (prod nat (prod nat nat))
 ETA x y : nat, Nat.add
      : nat -> nat -> nat
@@ -174,9 +173,8 @@ forall_non_null x y z t : nat , x = y /\ z = t
      : nat * (nat * nat) * (nat * nat * nat) * (nat * (nat * nat)) *
        (nat * nat * nat)
 pair
-  (pair
-     (pair (pair (S (S O)) (pair (S O) O)) (pair (pair O (S (S O))) (S O)))
-     (pair (S O) (pair (S (S O)) O))) (pair (pair O (S O)) (S (S O)))
+  (pair (pair (pair 2 (pair 1 0)) (pair (pair 0 2) 1)) (pair 1 (pair 2 0)))
+  (pair (pair 0 1) 2)
      : prod
          (prod (prod (prod nat (prod nat nat)) (prod (prod nat nat) nat))
             (prod nat (prod nat nat))) (prod (prod nat nat) nat)
@@ -238,7 +236,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/Notations4.out b/test-suite/output/Notations4.out
index 3477a293e3..0b18981f4e 100644
--- a/test-suite/output/Notations4.out
+++ b/test-suite/output/Notations4.out
@@ -77,18 +77,18 @@ fun x : nat => [x]
      : nat -> nat
 ∀ x : nat, x = x
      : Prop
-File "stdin", line 184, characters 0-160:
+File "stdin", line 187, characters 0-160:
 Warning: Notation "∀ _ .. _ , _" was already defined with a different format
 in scope type_scope. [notation-incompatible-format,parsing]
 ∀x : nat,x = x
      : Prop
-File "stdin", line 197, characters 0-60:
+File "stdin", line 200, characters 0-60:
 Warning: Notation "_ %%% _" was already defined with a different format.
 [notation-incompatible-format,parsing]
-File "stdin", line 201, characters 0-64:
+File "stdin", line 204, characters 0-64:
 Warning: Notation "_ %%% _" was already defined with a different format.
 [notation-incompatible-format,parsing]
-File "stdin", line 206, characters 0-62:
+File "stdin", line 209, characters 0-62:
 Warning: Lonely notation "_ %%%% _" was already defined with a different
 format. [notation-incompatible-format,parsing]
 3  %%  4
@@ -97,10 +97,10 @@ format. [notation-incompatible-format,parsing]
      : nat
 3   %%   4
      : nat
-File "stdin", line 234, characters 0-61:
+File "stdin", line 237, characters 0-61:
 Warning: The format modifier is irrelevant for only parsing rules.
 [irrelevant-format-only-parsing,parsing]
-File "stdin", line 238, characters 0-63:
+File "stdin", line 241, characters 0-63:
 Warning: The only parsing modifier has no effect in Reserved Notation.
 [irrelevant-reserved-notation-only-parsing,parsing]
 fun x : nat => U (S x)
@@ -111,7 +111,7 @@ fun x : nat => V x
      : forall x : nat, nat * (?T -> ?T)
 where
 ?T : [x : nat  x0 : ?T |- Type] (x0 cannot be used)
-File "stdin", line 255, characters 0-30:
+File "stdin", line 258, characters 0-30:
 Warning: Notation "_ :=: _" was already used. [notation-overridden,parsing]
 0 :=: 0
      : Prop
diff --git a/test-suite/output/Notations4.v b/test-suite/output/Notations4.v
index ebad12af88..a5ec92fe3c 100644
--- a/test-suite/output/Notations4.v
+++ b/test-suite/output/Notations4.v
@@ -103,7 +103,10 @@ Module NumberNotations.
     Delimit Scope test17_scope with test17.
     Local Set Primitive Projections.
     Record myint63 := of_int { to_int : int }.
-    Number Notation myint63 of_int to_int : test17_scope.
+    Definition parse x :=
+      match x with Pos x => Some (of_int x) | Neg _ => None end.
+    Definition print x := Pos (to_int x).
+    Number Notation myint63 parse print : test17_scope.
     Check let v := 0%test17 in v : myint63.
   End Test17.
 End NumberNotations.
diff --git a/test-suite/output/NumberNotations.out b/test-suite/output/NumberNotations.out
index 60682edec8..df9b39389c 100644
--- a/test-suite/output/NumberNotations.out
+++ b/test-suite/output/NumberNotations.out
@@ -260,28 +260,28 @@ The command has indeed failed with message:
 add is not a constructor of an inductive type.
 The command has indeed failed with message:
 Missing mapping for constructor Iempty.
-File "stdin", line 574, characters 56-61:
+File "stdin", line 577, characters 56-61:
 Warning: Type of I'sum seems incompatible with the type of sum.
 Expected type is: (I' -> I' -> I') instead of (I -> I' -> I').
 This might yield ill typed terms when using the notation.
 [via-type-mismatch,numbers]
-File "stdin", line 579, characters 32-33:
+File "stdin", line 582, characters 32-33:
 Warning: I was already mapped to Set, mapping it also to
 nat might yield ill typed terms when using the notation.
 [via-type-remapping,numbers]
-File "stdin", line 579, characters 37-42:
+File "stdin", line 582, characters 37-42:
 Warning: Type of Iunit seems incompatible with the type of O.
 Expected type is: I instead of I.
 This might yield ill typed terms when using the notation.
 [via-type-mismatch,numbers]
 The command has indeed failed with message:
 'via' and 'abstract' cannot be used together.
-File "stdin", line 659, characters 21-23:
+File "stdin", line 662, characters 21-23:
 Warning: Type of I1 seems incompatible with the type of Fin.F1.
 Expected type is: (nat -> I) instead of I.
 This might yield ill typed terms when using the notation.
 [via-type-mismatch,numbers]
-File "stdin", line 659, characters 35-37:
+File "stdin", line 662, characters 35-37:
 Warning: Type of IS seems incompatible with the type of Fin.FS.
 Expected type is: (nat -> I -> I) instead of (I -> I).
 This might yield ill typed terms when using the notation.
diff --git a/test-suite/output/NumberNotations.v b/test-suite/output/NumberNotations.v
index 718da13500..85400c2fd4 100644
--- a/test-suite/output/NumberNotations.v
+++ b/test-suite/output/NumberNotations.v
@@ -328,7 +328,10 @@ Module Test17.
   Delimit Scope test17_scope with test17.
   Local Set Primitive Projections.
   Record myint63 := of_int { to_int : int }.
-  Number Notation myint63 of_int to_int : test17_scope.
+  Definition parse x :=
+    match x with Pos x => Some (of_int x) | Neg _ => None end.
+  Definition print x := Pos (to_int x).
+  Number Notation myint63 parse print : test17_scope.
   Check let v := 0%test17 in v : myint63.
 End Test17.
 
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/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/Sint63Syntax.out b/test-suite/output/Sint63Syntax.out
new file mode 100644
index 0000000000..db14658307
--- /dev/null
+++ b/test-suite/output/Sint63Syntax.out
@@ -0,0 +1,66 @@
+2%sint63
+     : int
+2
+     : int
+-3
+     : int
+4611686018427387903
+     : int
+-4611686018427387904
+     : int
+427
+     : int
+427
+     : int
+427
+     : int
+427
+     : int
+427
+     : int
+The command has indeed failed with message:
+Cannot interpret this number as a value of type int
+The command has indeed failed with message:
+Cannot interpret this number as a value of type int
+0
+     : int
+0
+     : int
+The command has indeed failed with message:
+The reference xg was not found in the current environment.
+The command has indeed failed with message:
+The reference xG was not found in the current environment.
+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
+The command has indeed failed with message:
+Cannot interpret this number as a value of type int
+The command has indeed failed with message:
+Cannot interpret this number as a value of type int
+0x1%int63
+     : int
+0x7fffffffffffffff%int63
+     : int
+2
+     : nat
+2%sint63
+     : int
+t = 2%si63
+     : int
+t = 2%si63
+     : int
+2
+     : nat
+2
+     : int
+(2 + 2)%sint63
+     : int
+2 + 2
+     : int
+     = 4
+     : int
+     = 37151199385380486
+     : int
diff --git a/test-suite/output/Sint63Syntax.v b/test-suite/output/Sint63Syntax.v
new file mode 100644
index 0000000000..b9ed596537
--- /dev/null
+++ b/test-suite/output/Sint63Syntax.v
@@ -0,0 +1,49 @@
+Require Import Sint63.
+
+Check 2%sint63.
+Open Scope sint63_scope.
+Check 2.
+Check -3.
+Check 4611686018427387903.
+Check -4611686018427387904.
+Check 0x1ab.
+Check 0X1ab.
+Check 0x1Ab.
+Check 0x1aB.
+Check 0x1AB.
+Fail Check 0x1ap5.  (* exponents not implemented (yet?) *)
+Fail Check 0x1aP5.
+Check 0x0.
+Check 0x000.
+Fail Check 0xg.
+Fail Check 0xG.
+Fail Check 00x1.
+Fail Check 0x.
+Check (PrimInt63.add 2 2).
+Fail Check 4611686018427387904.
+Fail Check -4611686018427387905.
+
+Set Printing All.
+Check 1%sint63.
+Check (-1)%sint63.
+Unset Printing All.
+
+Open Scope nat_scope.
+Check 2. (* : nat *)
+Check 2%sint63.
+Delimit Scope sint63_scope with si63.
+Definition t := 2%sint63.
+Print t.
+Delimit Scope nat_scope with sint63.
+Print t.
+Check 2.
+Close Scope nat_scope.
+Check 2.
+Close Scope sint63_scope.
+Delimit Scope sint63_scope with sint63.
+
+Check (2 + 2)%sint63.
+Open Scope sint63_scope.
+Check (2+2).
+Eval vm_compute in 2+2.
+Eval vm_compute in 65675757 * 565675998.
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 95b6c6ee95..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
diff --git a/test-suite/output/bug_13821_native_command_line_warn.out b/test-suite/output/bug_13821_native_command_line_warn.out
new file mode 100644
index 0000000000..e69de29bb2
--- /dev/null
+++ b/test-suite/output/bug_13821_native_command_line_warn.out
diff --git a/test-suite/output/bug_13821_native_command_line_warn.v b/test-suite/output/bug_13821_native_command_line_warn.v
new file mode 100644
index 0000000000..a28210b6c2
--- /dev/null
+++ b/test-suite/output/bug_13821_native_command_line_warn.v
@@ -0,0 +1 @@
+(* -*- coq-prog-args: ("-w" "-native-compiler-disabled" "-native-compiler" "ondemand"); -*- *)
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/primitive_tokens.out b/test-suite/output/primitive_tokens.out
new file mode 100644
index 0000000000..afe9b25442
--- /dev/null
+++ b/test-suite/output/primitive_tokens.out
@@ -0,0 +1,61 @@
+"foo"
+     : string
+1234
+     : nat
+Nat.add 1 2
+     : nat
+match "a" with
+| "a" => true
+| _ => false
+end
+     : bool
+match 1 with
+| 1 => true
+| _ => false
+end
+     : bool
+{| field := 7 |}
+     : test
+String (Ascii.Ascii false true true false false true true false)
+  (String (Ascii.Ascii true true true true false true true false)
+     (String (Ascii.Ascii true true true true false true true false)
+        EmptyString))
+     : string
+S
+  (S
+     (S
+        (S
+           (S
+              (S
+                 (S
+                    (S
+                       (S
+                          (S
+                             (S
+                                (S
+                                   (S
+                                      (S
+                                         (S
+                                            (S
+                                               (S
+                                                 (S
+                                                 (S (S (S (S (S (S ...)))))))))))))))))))))))
+     : nat
+Nat.add (S O) (S (S O))
+     : nat
+match
+  String (Ascii.Ascii true false false false false true true false)
+    EmptyString
+with
+| String (Ascii.Ascii true false false false false true true false)
+  EmptyString => true
+| _ => false
+end
+     : bool
+match S O with
+| S O => true
+| _ => false
+end
+     : bool
+{| field := S (S (S (S (S (S (S O)))))) |}
+     : test
diff --git a/test-suite/output/primitive_tokens.v b/test-suite/output/primitive_tokens.v
new file mode 100644
index 0000000000..3207e5983f
--- /dev/null
+++ b/test-suite/output/primitive_tokens.v
@@ -0,0 +1,23 @@
+Require Import String.
+
+Record test := { field : nat }.
+
+Open Scope string_scope.
+
+Unset Printing Notations.
+
+Check "foo".
+Check 1234.
+Check 1 + 2.
+Check match "a" with "a" => true | _ => false end.
+Check match 1 with 1 => true | _ => false end.
+Check {| field := 7 |}.
+
+Set Printing Raw Literals.
+
+Check "foo".
+Check 1234.
+Check 1 + 2.
+Check match "a" with "a" => true | _ => false end.
+Check match 1 with 1 => true | _ => false end.
+Check {| field := 7 |}.
diff --git a/test-suite/output/relaxed_ambiguous_paths.out b/test-suite/output/relaxed_ambiguous_paths.out
index ac5a09bad7..48368c7ede 100644
--- a/test-suite/output/relaxed_ambiguous_paths.out
+++ b/test-suite/output/relaxed_ambiguous_paths.out
@@ -3,32 +3,32 @@ Warning:
 New coercion path [ac; cd] : A >-> D is ambiguous with existing 
 [ab; bd] : A >-> D. [ambiguous-paths,typechecker]
 [ab] : A >-> B
-[ab; bd] : A >-> D
 [ac] : A >-> C
+[ab; bd] : A >-> D
 [bd] : B >-> D
 [cd] : C >-> D
 File "stdin", line 26, characters 0-28:
 Warning:
 New coercion path [ab; bc] : A >-> C is ambiguous with existing 
 [ac] : A >-> C. [ambiguous-paths,typechecker]
+[ab] : A >-> B
 [ac] : A >-> C
 [ac; cd] : A >-> D
-[ab] : A >-> B
-[cd] : C >-> D
 [bc] : B >-> C
 [bc; cd] : B >-> D
+[cd] : C >-> D
 [B_A] : B >-> A
 [C_A] : C >-> A
-[D_B] : D >-> B
 [D_A] : D >-> A
+[D_B] : D >-> B
 [D_C] : D >-> C
 [A'_A] : A' >-> A
-[B_A'] : B >-> A'
 [B_A'; A'_A] : B >-> A
-[C_A'] : C >-> A'
+[B_A'] : B >-> A'
 [C_A'; A'_A] : C >-> A
-[D_B; B_A'] : D >-> A'
+[C_A'] : C >-> A'
 [D_A] : D >-> A
+[D_B; B_A'] : D >-> A'
 [D_B] : D >-> B
 [D_C] : D >-> C
 File "stdin", line 121, characters 0-86:
@@ -36,12 +36,12 @@ Warning:
 New coercion path [D_C; C_A'] : D >-> A' is ambiguous with existing 
 [D_B; B_A'] : D >-> A'. [ambiguous-paths,typechecker]
 [A'_A] : A' >-> A
-[B_A'] : B >-> A'
 [B_A'; A'_A] : B >-> A
-[C_A'] : C >-> A'
+[B_A'] : B >-> A'
 [C_A'; A'_A] : C >-> A
-[D_B; B_A'] : D >-> A'
+[C_A'] : C >-> A'
 [D_A] : D >-> A
+[D_B; B_A'] : D >-> A'
 [D_B] : D >-> B
 [D_C] : D >-> C
 File "stdin", line 130, characters 0-47:
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/sint63/add.v b/test-suite/primitive/sint63/add.v
new file mode 100644
index 0000000000..dcafd64181
--- /dev/null
+++ b/test-suite/primitive/sint63/add.v
@@ -0,0 +1,25 @@
+Require Import Sint63.
+
+Set Implicit Arguments.
+
+Open Scope sint63_scope.
+
+Check (eq_refl : 2 + 3 = 5).
+Check (eq_refl 5 <: 2 + 3 = 5).
+Check (eq_refl 5 <<: 2 + 3 = 5).
+Definition compute1 := Eval compute in 2 + 3.
+Check (eq_refl compute1 : 5 = 5).
+
+Check (eq_refl : 4611686018427387903 + 1 = -4611686018427387904).
+Check (eq_refl (-4611686018427387904) <:
+  4611686018427387903 + 1 = -4611686018427387904).
+Check (eq_refl (-4611686018427387904) <<:
+  4611686018427387903 + 1 = -4611686018427387904).
+Definition compute2 := Eval compute in 4611686018427387903 + 1.
+Check (eq_refl compute2 : -4611686018427387904 = -4611686018427387904).
+
+Check (eq_refl : 2 - 3 = -1).
+Check (eq_refl (-1) <: 2 - 3 = -1).
+Check (eq_refl (-1) <<: 2 - 3 = -1).
+Definition compute3 := Eval compute in 2 - 3.
+Check (eq_refl compute3 : -1 = -1).
diff --git a/test-suite/primitive/sint63/asr.v b/test-suite/primitive/sint63/asr.v
new file mode 100644
index 0000000000..4524ae4e6f
--- /dev/null
+++ b/test-suite/primitive/sint63/asr.v
@@ -0,0 +1,41 @@
+Require Import Sint63.
+
+Set Implicit Arguments.
+
+Open Scope sint63_scope.
+
+Check (eq_refl : (-2305843009213693952) >> 61 = -1).
+Check (eq_refl (-1) <: (-2305843009213693952) >> 61 = -1).
+Check (eq_refl (-1) <<: (-2305843009213693952) >> 61 = -1).
+Definition compute1 := Eval compute in (-2305843009213693952) >> 61.
+Check (eq_refl compute1 : -1 = -1).
+
+Check (eq_refl : 2305843009213693952 >> 62 = 0).
+Check (eq_refl 0 <: 2305843009213693952 >> 62 = 0).
+Check (eq_refl 0 <<: 2305843009213693952 >> 62 = 0).
+Definition compute2 := Eval compute in 2305843009213693952 >> 62.
+Check (eq_refl compute2 : 0 = 0).
+
+Check (eq_refl : 4611686018427387903 >> 63 = 0).
+Check (eq_refl 0 <: 4611686018427387903 >> 63 = 0).
+Check (eq_refl 0 <<: 4611686018427387903 >> 63 = 0).
+Definition compute3 := Eval compute in 4611686018427387903 >> 63.
+Check (eq_refl compute3 : 0 = 0).
+
+Check (eq_refl : (-1) >> 1 = -1).
+Check (eq_refl (-1) <: (-1) >> 1 = -1).
+Check (eq_refl (-1) <<: (-1) >> 1 = -1).
+Definition compute4 := Eval compute in (-1) >> 1.
+Check (eq_refl compute4 : -1 = -1).
+
+Check (eq_refl : (-1) >> (-1) = 0).
+Check (eq_refl 0 <: (-1) >> (-1) = 0).
+Check (eq_refl 0 <<: (-1) >> (-1) = 0).
+Definition compute5 := Eval compute in (-1) >> (-1).
+Check (eq_refl compute5 : 0 = 0).
+
+Check (eq_refl : 73 >> (-2) = 0).
+Check (eq_refl 0 <: 73 >> (-2) = 0).
+Check (eq_refl 0 <<: 73 >> (-2) = 0).
+Definition compute6 := Eval compute in 73 >> (-2).
+Check (eq_refl compute6 : 0 = 0).
diff --git a/test-suite/primitive/sint63/compare.v b/test-suite/primitive/sint63/compare.v
new file mode 100644
index 0000000000..7a9882f1c8
--- /dev/null
+++ b/test-suite/primitive/sint63/compare.v
@@ -0,0 +1,36 @@
+Require Import Sint63.
+
+Set Implicit Arguments.
+
+Open Scope sint63_scope.
+
+Check (eq_refl : 1 ?= 1 = Eq).
+Check (eq_refl Eq <: 1 ?= 1 = Eq).
+Check (eq_refl Eq <<: 1 ?= 1 = Eq).
+Definition compute1 := Eval compute in 1 ?= 1.
+Check (eq_refl compute1 : Eq = Eq).
+
+Check (eq_refl : 1 ?= 2 = Lt).
+Check (eq_refl Lt <: 1 ?= 2 = Lt).
+Check (eq_refl Lt <<: 1 ?= 2 = Lt).
+Definition compute2 := Eval compute in 1 ?= 2.
+Check (eq_refl compute2 : Lt = Lt).
+
+Check (eq_refl : 4611686018427387903 ?= 0 = Gt).
+Check (eq_refl Gt <: 4611686018427387903 ?= 0 = Gt).
+Check (eq_refl Gt <<: 4611686018427387903 ?= 0 = Gt).
+Definition compute3 := Eval compute in 4611686018427387903 ?= 0.
+Check (eq_refl compute3 : Gt = Gt).
+
+Check (eq_refl : -1 ?= 1 = Lt).
+Check (eq_refl Lt <: -1 ?= 1 = Lt).
+Check (eq_refl Lt <<: -1 ?= 1 = Lt).
+Definition compute4 := Eval compute in -1 ?= 1.
+Check (eq_refl compute4 : Lt = Lt).
+
+Check (eq_refl : 4611686018427387903 ?= -4611686018427387904 = Gt).
+Check (eq_refl Gt <: 4611686018427387903 ?= -4611686018427387904 = Gt).
+Check (eq_refl Gt <<: 4611686018427387903 ?= -4611686018427387904 = Gt).
+Definition compute5 :=
+  Eval compute in 4611686018427387903 ?= -4611686018427387904.
+Check (eq_refl compute5 : Gt = Gt).
diff --git a/test-suite/primitive/sint63/div.v b/test-suite/primitive/sint63/div.v
new file mode 100644
index 0000000000..9da628ce1e
--- /dev/null
+++ b/test-suite/primitive/sint63/div.v
@@ -0,0 +1,61 @@
+Require Import Sint63.
+
+Set Implicit Arguments.
+
+Open Scope sint63_scope.
+
+Check (eq_refl : 6 / 3 = 2).
+Check (eq_refl 2 <: 6 / 3 = 2).
+Check (eq_refl 2 <<: 6 / 3 = 2).
+Definition compute1 := Eval compute in 6 / 3.
+Check (eq_refl compute1 : 2 = 2).
+
+Check (eq_refl : -6 / 3 = -2).
+Check (eq_refl (-2) <: -6 / 3 = -2).
+Check (eq_refl (-2) <<: -6 / 3 = -2).
+Definition compute2 := Eval compute in -6 / 3.
+Check (eq_refl compute2 : -2 = -2).
+
+Check (eq_refl : 6 / -3 = -2).
+Check (eq_refl (-2) <: 6 / -3 = -2).
+Check (eq_refl (-2) <<: 6 / -3 = -2).
+Definition compute3 := Eval compute in 6 / -3.
+Check (eq_refl compute3 : -2 = -2).
+
+Check (eq_refl : -6 / -3 = 2).
+Check (eq_refl 2 <: -6 / -3 = 2).
+Check (eq_refl 2 <<: -6 / -3 = 2).
+Definition compute4 := Eval compute in -6 / -3.
+Check (eq_refl compute4 : 2 = 2).
+
+Check (eq_refl : 3 / 2 = 1).
+Check (eq_refl 1 <: 3 / 2 = 1).
+Check (eq_refl 1 <<: 3 / 2 = 1).
+Definition compute5 := Eval compute in 3 / 2.
+Check (eq_refl compute5 : 1 = 1).
+
+Check (eq_refl : -3 / 2 = -1).
+Check (eq_refl (-1) <: -3 / 2 = -1).
+Check (eq_refl (-1) <<: -3 / 2 = -1).
+Definition compute6 := Eval compute in -3 / 2.
+Check (eq_refl compute6 : -1 = -1).
+
+Check (eq_refl : 3 / -2 = -1).
+Check (eq_refl (-1) <: 3 / -2 = -1).
+Check (eq_refl (-1) <<: 3 / -2 = -1).
+Definition compute7 := Eval compute in 3 / -2.
+Check (eq_refl compute7 : -1 = -1).
+
+Check (eq_refl : -3 / -2 = 1).
+Check (eq_refl 1 <: -3 / -2 = 1).
+Check (eq_refl 1 <<: -3 / -2 = 1).
+Definition compute8 := Eval compute in -3 / -2.
+Check (eq_refl compute8 : 1 = 1).
+
+Check (eq_refl : -4611686018427387904 / -1 = -4611686018427387904).
+Check (eq_refl (-4611686018427387904) <:
+  -4611686018427387904 / -1 = -4611686018427387904).
+Check (eq_refl (-4611686018427387904) <<:
+  -4611686018427387904 / -1 = -4611686018427387904).
+Definition compute9 := Eval compute in -4611686018427387904 / -1.
+Check (eq_refl compute9 : -4611686018427387904 = -4611686018427387904).
diff --git a/test-suite/primitive/sint63/eqb.v b/test-suite/primitive/sint63/eqb.v
new file mode 100644
index 0000000000..4d365acf54
--- /dev/null
+++ b/test-suite/primitive/sint63/eqb.v
@@ -0,0 +1,17 @@
+Require Import Sint63.
+
+Set Implicit Arguments.
+
+Open Scope sint63_scope.
+
+Check (eq_refl : 1 =? 1 = true).
+Check (eq_refl true <: 1 =? 1 = true).
+Check (eq_refl true <<: 1 =? 1 = true).
+Definition compute1 := Eval compute in 1 =? 1.
+Check (eq_refl compute1 : true = true).
+
+Check (eq_refl : 4611686018427387903 =? 0 = false).
+Check (eq_refl false <: 4611686018427387903 =? 0 = false).
+Check (eq_refl false <<: 4611686018427387903 =? 0 = false).
+Definition compute2 := Eval compute in 4611686018427387903 =? 0.
+Check (eq_refl compute2 : false = false).
diff --git a/test-suite/primitive/sint63/isint.v b/test-suite/primitive/sint63/isint.v
new file mode 100644
index 0000000000..f1c9c2cfd1
--- /dev/null
+++ b/test-suite/primitive/sint63/isint.v
@@ -0,0 +1,50 @@
+(* This file tests the check that arithmetic operations use to know if their
+arguments are ground. The various test cases correspond to possible
+optimizations of these tests made by the compiler. *)
+Require Import Sint63.
+
+Set Implicit Arguments.
+
+Open Scope sint63_scope.
+
+Section test.
+
+Variable m n : int.
+
+Check (eq_refl : (fun x => x + 3) m = m + 3).
+Check (eq_refl (m + 3) <: (fun x => x + 3) m = m + 3).
+Check (eq_refl (m + 3) <<: (fun x => x + 3) m = m + 3).
+Definition compute1 := Eval compute in (fun x => x + 3) m.
+Check (eq_refl compute1 : m + 3 = m + 3).
+
+Check (eq_refl : (fun x => 3 + x) m = 3 + m).
+Check (eq_refl (3 + m) <: (fun x => 3 + x) m = 3 + m).
+Check (eq_refl (3 + m) <<: (fun x => 3 + x) m = 3 + m).
+Definition compute2 := Eval compute in (fun x => 3 + x) m.
+Check (eq_refl compute2 : 3 + m = 3 + m).
+
+Check (eq_refl : (fun x y => x + y) m n = m + n).
+Check (eq_refl (m + n) <: (fun x y => x + y) m n = m + n).
+Check (eq_refl (m + n) <<: (fun x y => x + y) m n = m + n).
+Definition compute3 := Eval compute in (fun x y => x + y) m n.
+Check (eq_refl compute3 : m + n = m + n).
+
+Check (eq_refl : (fun x y => x + y) 2 3 = 5).
+Check (eq_refl 5 <: (fun x y => x + y) 2 3 = 5).
+Check (eq_refl 5 <<: (fun x y => x + y) 2 3 = 5).
+Definition compute4 := Eval compute in (fun x y => x + y) 2 3.
+Check (eq_refl compute4 : 5 = 5).
+
+Check (eq_refl : (fun x => x + x) m = m + m).
+Check (eq_refl (m + m) <: (fun x => x + x) m = m + m).
+Check (eq_refl (m + m) <<: (fun x => x + x) m = m + m).
+Definition compute5 := Eval compute in (fun x => x + x) m.
+Check (eq_refl compute5 : m + m = m + m).
+
+Check (eq_refl : (fun x => x + x) 2 = 4).
+Check (eq_refl 4 <: (fun x => x + x) 2 = 4).
+Check (eq_refl 4 <<: (fun x => x + x) 2 = 4).
+Definition compute6 := Eval compute in (fun x => x + x) 2.
+Check (eq_refl compute6 : 4 = 4).
+
+End test.
diff --git a/test-suite/primitive/sint63/leb.v b/test-suite/primitive/sint63/leb.v
new file mode 100644
index 0000000000..dbe958e41d
--- /dev/null
+++ b/test-suite/primitive/sint63/leb.v
@@ -0,0 +1,29 @@
+Require Import Sint63.
+
+Set Implicit Arguments.
+
+Open Scope sint63_scope.
+
+Check (eq_refl : 1 <=? 1 = true).
+Check (eq_refl true <: 1 <=? 1 = true).
+Check (eq_refl true <<: 1 <=? 1 = true).
+Definition compute1 := Eval compute in 1 <=? 1.
+Check (eq_refl compute1 : true = true).
+
+Check (eq_refl : 1 <=? 2 = true).
+Check (eq_refl true <: 1 <=? 2 = true).
+Check (eq_refl true <<: 1 <=? 2 = true).
+Definition compute2 := Eval compute in 1 <=? 2.
+Check (eq_refl compute2 : true = true).
+
+Check (eq_refl : 4611686018427387903 <=? 0 = false).
+Check (eq_refl false <: 4611686018427387903 <=? 0 = false).
+Check (eq_refl false <<: 4611686018427387903 <=? 0 = false).
+Definition compute3 := Eval compute in 4611686018427387903 <=? 0.
+Check (eq_refl compute3 : false = false).
+
+Check (eq_refl : 1 <=? -1 = false).
+Check (eq_refl false <: 1 <=? -1 = false).
+Check (eq_refl false <<: 1 <=? -1 = false).
+Definition compute4 := Eval compute in 1 <=? -1.
+Check (eq_refl compute4 : false = false).
diff --git a/test-suite/primitive/sint63/lsl.v b/test-suite/primitive/sint63/lsl.v
new file mode 100644
index 0000000000..082c42979a
--- /dev/null
+++ b/test-suite/primitive/sint63/lsl.v
@@ -0,0 +1,43 @@
+Require Import Sint63.
+
+Set Implicit Arguments.
+
+Open Scope sint63_scope.
+
+Check (eq_refl : 3 << 61 = -2305843009213693952).
+Check (eq_refl (-2305843009213693952) <: 3 << 61 = -2305843009213693952).
+Check (eq_refl (-2305843009213693952) <<: 3 << 61 = -2305843009213693952).
+Definition compute1 := Eval compute in 3 << 61.
+Check (eq_refl compute1 : -2305843009213693952 = -2305843009213693952).
+
+Check (eq_refl : 2 << 62 = 0).
+Check (eq_refl 0 <: 2 << 62 = 0).
+Check (eq_refl 0 <<: 2 << 62 = 0).
+Definition compute2 := Eval compute in 2 << 62.
+Check (eq_refl compute2 : 0 = 0).
+
+Check (eq_refl : 4611686018427387903 << 63 = 0).
+Check (eq_refl 0 <: 4611686018427387903 << 63 = 0).
+Check (eq_refl 0 <<: 4611686018427387903 << 63 = 0).
+Definition compute3 := Eval compute in 4611686018427387903 << 63.
+Check (eq_refl compute3 : 0 = 0).
+
+Check (eq_refl : 4611686018427387903 << 62 = -4611686018427387904).
+Check (eq_refl (-4611686018427387904) <:
+  4611686018427387903 << 62 = -4611686018427387904).
+Check (eq_refl (-4611686018427387904) <<:
+  4611686018427387903 << 62 = -4611686018427387904).
+Definition compute4 := Eval compute in 4611686018427387903 << 62.
+Check (eq_refl compute4 : -4611686018427387904 = -4611686018427387904).
+
+Check (eq_refl : 1 << 62 = -4611686018427387904).
+Check (eq_refl (-4611686018427387904) <: 1 << 62 = -4611686018427387904).
+Check (eq_refl (-4611686018427387904) <<: 1 << 62 = -4611686018427387904).
+Definition compute5 := Eval compute in 1 << 62.
+Check (eq_refl compute5 : -4611686018427387904 = -4611686018427387904).
+
+Check (eq_refl : -1 << 1 = -2).
+Check (eq_refl (-2) <: -1 << 1 = -2).
+Check (eq_refl (-2) <<: -1 << 1 = -2).
+Definition compute6 := Eval compute in -1 << 1.
+Check (eq_refl compute6 : -2 = -2).
diff --git a/test-suite/primitive/sint63/ltb.v b/test-suite/primitive/sint63/ltb.v
new file mode 100644
index 0000000000..aa72e1d377
--- /dev/null
+++ b/test-suite/primitive/sint63/ltb.v
@@ -0,0 +1,29 @@
+Require Import Sint63.
+
+Set Implicit Arguments.
+
+Open Scope sint63_scope.
+
+Check (eq_refl : 1 <? 1 = false).
+Check (eq_refl false <: 1 <? 1 = false).
+Check (eq_refl false <<: 1 <? 1 = false).
+Definition compute1 := Eval compute in 1 <? 1.
+Check (eq_refl compute1 : false = false).
+
+Check (eq_refl : 1 <? 2 = true).
+Check (eq_refl true <: 1 <? 2 = true).
+Check (eq_refl true <<: 1 <? 2 = true).
+Definition compute2 := Eval compute in 1 <? 2.
+Check (eq_refl compute2 : true = true).
+
+Check (eq_refl : 4611686018427387903 <? 0 = false).
+Check (eq_refl false <: 4611686018427387903 <? 0 = false).
+Check (eq_refl false <<: 4611686018427387903 <? 0 = false).
+Definition compute3 := Eval compute in 4611686018427387903 <? 0.
+Check (eq_refl compute3 : false = false).
+
+Check (eq_refl : 1 <? -1 = false).
+Check (eq_refl false <: 1 <? -1 = false).
+Check (eq_refl false <<: 1 <? -1 = false).
+Definition compute4 := Eval compute in 1 <? -1.
+Check (eq_refl compute4 : false = false).
diff --git a/test-suite/primitive/sint63/mod.v b/test-suite/primitive/sint63/mod.v
new file mode 100644
index 0000000000..a4872b45f3
--- /dev/null
+++ b/test-suite/primitive/sint63/mod.v
@@ -0,0 +1,53 @@
+Require Import Sint63.
+
+Set Implicit Arguments.
+
+Open Scope sint63_scope.
+
+Check (eq_refl : 6 mod 3 = 0).
+Check (eq_refl 0 <: 6 mod 3 = 0).
+Check (eq_refl 0 <<: 6 mod 3 = 0).
+Definition compute1 := Eval compute in 6 mod 3.
+Check (eq_refl compute1 : 0 = 0).
+
+Check (eq_refl : -6 mod 3 = 0).
+Check (eq_refl 0 <: -6 mod 3 = 0).
+Check (eq_refl 0 <<: -6 mod 3 = 0).
+Definition compute2 := Eval compute in -6 mod 3.
+Check (eq_refl compute2 : 0 = 0).
+
+Check (eq_refl : 6 mod -3 = 0).
+Check (eq_refl 0 <: 6 mod -3 = 0).
+Check (eq_refl 0 <<: 6 mod -3 = 0).
+Definition compute3 := Eval compute in 6 mod -3.
+Check (eq_refl compute3 : 0 = 0).
+
+Check (eq_refl : -6 mod -3 = 0).
+Check (eq_refl 0 <: -6 mod -3 = 0).
+Check (eq_refl 0 <<: -6 mod -3 = 0).
+Definition compute4 := Eval compute in -6 mod -3.
+Check (eq_refl compute4 : 0 = 0).
+
+Check (eq_refl : 5 mod 3 = 2).
+Check (eq_refl 2 <: 5 mod 3 = 2).
+Check (eq_refl 2 <<: 5 mod 3 = 2).
+Definition compute5 := Eval compute in 5 mod 3.
+Check (eq_refl compute5 : 2 = 2).
+
+Check (eq_refl : -5 mod 3 = -2).
+Check (eq_refl (-2) <: -5 mod 3 = -2).
+Check (eq_refl (-2) <<: -5 mod 3 = -2).
+Definition compute6 := Eval compute in -5 mod 3.
+Check (eq_refl compute6 : -2 = -2).
+
+Check (eq_refl : 5 mod -3 = 2).
+Check (eq_refl 2 <: 5 mod -3 = 2).
+Check (eq_refl 2 <<: 5 mod -3 = 2).
+Definition compute7 := Eval compute in 5 mod -3.
+Check (eq_refl compute7 : 2 = 2).
+
+Check (eq_refl : -5 mod -3 = -2).
+Check (eq_refl (-2) <: -5 mod -3 = -2).
+Check (eq_refl (-2) <<: -5 mod -3 = -2).
+Definition compute8 := Eval compute in -5 mod -3.
+Check (eq_refl compute8 : -2 = -2).
diff --git a/test-suite/primitive/sint63/mul.v b/test-suite/primitive/sint63/mul.v
new file mode 100644
index 0000000000..f72f643083
--- /dev/null
+++ b/test-suite/primitive/sint63/mul.v
@@ -0,0 +1,35 @@
+Require Import Sint63.
+
+Set Implicit Arguments.
+
+Open Scope sint63_scope.
+
+Check (eq_refl : 2 * 3 = 6).
+Check (eq_refl 6 <: 2 * 3 = 6).
+Check (eq_refl 6 <<: 2 * 3 = 6).
+Definition compute1 := Eval compute in 2 * 3.
+Check (eq_refl compute1 : 6 = 6).
+
+Check (eq_refl : -2 * 3 = -6).
+Check (eq_refl (-6) <: -2 * 3 = -6).
+Check (eq_refl (-6) <<: -2 * 3 = -6).
+Definition compute2 := Eval compute in -2 * 3.
+Check (eq_refl compute2 : -6 = -6).
+
+Check (eq_refl : 2 * -3 = -6).
+Check (eq_refl (-6) <: 2 * -3 = -6).
+Check (eq_refl (-6) <<: 2 * -3 = -6).
+Definition compute3 := Eval compute in 2 * -3.
+Check (eq_refl compute3 : -6 = -6).
+
+Check (eq_refl : -2 * -3 = 6).
+Check (eq_refl 6 <: -2 * -3 = 6).
+Check (eq_refl 6 <<: -2 * -3 = 6).
+Definition compute4 := Eval compute in -2 * -3.
+Check (eq_refl compute4 : 6 = 6).
+
+Check (eq_refl : 4611686018427387903 * 2 = -2).
+Check (eq_refl (-2) <: 4611686018427387903 * 2 = -2).
+Check (eq_refl (-2) <<: 4611686018427387903 * 2 = -2).
+Definition compute5 := Eval compute in 4611686018427387903 * 2.
+Check (eq_refl compute5 : -2 = -2).
diff --git a/test-suite/primitive/sint63/signed.v b/test-suite/primitive/sint63/signed.v
new file mode 100644
index 0000000000..d8333a8efb
--- /dev/null
+++ b/test-suite/primitive/sint63/signed.v
@@ -0,0 +1,18 @@
+(* This file checks that operations over sint63 are signed. *)
+Require Import Sint63.
+
+Open Scope sint63_scope.
+
+(* (0-1) must be negative 1 and not the maximum integer value *)
+
+Check (eq_refl : 1/(0-1) = -1).
+Check (eq_refl (-1) <: 1/(0-1) = -1).
+Check (eq_refl (-1) <<: 1/(0-1) = -1).
+Definition compute1 := Eval compute in 1/(0-1).
+Check (eq_refl compute1 : -1 = -1).
+
+Check (eq_refl : 3 mod (0-1) = 0).
+Check (eq_refl 0 <: 3 mod (0-1) = 0).
+Check (eq_refl 0 <<: 3 mod (0-1) = 0).
+Definition compute2 := Eval compute in 3 mod (0-1).
+Check (eq_refl compute2 : 0 = 0).
diff --git a/test-suite/primitive/sint63/sub.v b/test-suite/primitive/sint63/sub.v
new file mode 100644
index 0000000000..8504177286
--- /dev/null
+++ b/test-suite/primitive/sint63/sub.v
@@ -0,0 +1,25 @@
+Require Import Sint63.
+
+Set Implicit Arguments.
+
+Open Scope sint63_scope.
+
+Check (eq_refl : 3 - 2 = 1).
+Check (eq_refl 1 <: 3 - 2 = 1).
+Check (eq_refl 1 <<: 3 - 2 = 1).
+Definition compute1 := Eval compute in 3 - 2.
+Check (eq_refl compute1 : 1 = 1).
+
+Check (eq_refl : 0 - 1 = -1).
+Check (eq_refl (-1) <: 0 - 1 = -1).
+Check (eq_refl (-1) <<: 0 - 1 = -1).
+Definition compute2 := Eval compute in 0 - 1.
+Check (eq_refl compute2 : -1 = -1).
+
+Check (eq_refl : -4611686018427387904 - 1 = 4611686018427387903).
+Check (eq_refl 4611686018427387903 <:
+  -4611686018427387904 - 1 = 4611686018427387903).
+Check (eq_refl 4611686018427387903 <<:
+  -4611686018427387904 - 1 = 4611686018427387903).
+Definition compute3 := Eval compute in -4611686018427387904 - 1.
+Check (eq_refl compute3 : 4611686018427387903 = 4611686018427387903).
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/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.