22 files changed, 311 insertions, 137 deletions

diff --git a/test-suite/bugs/closed/bug_4502.v b/test-suite/bugs/closed/bug_4502.v
new file mode 100644
index 0000000000..f1dcae9773
--- /dev/null
+++ b/test-suite/bugs/closed/bug_4502.v
@@ -0,0 +1,17 @@
+Require Import FunInd.
+
+Set Universe Polymorphism.
+Set Primitive Projections.
+Set Implicit Arguments.
+Set Strongly Strict Implicit.
+
+Function first_false (n : nat) (f : nat -> bool) : option nat :=
+  match n with
+  | O => None
+  | S m =>
+    match first_false m f with
+    | (Some _) as s => s
+    | None => if f m then None else Some m
+    end
+  end.
+(* undefined universe *)
diff --git a/test-suite/bugs/closed/bug_9114.v b/test-suite/bugs/closed/bug_9114.v
new file mode 100644
index 0000000000..2cf91c1c2b
--- /dev/null
+++ b/test-suite/bugs/closed/bug_9114.v
@@ -0,0 +1,5 @@
+Goal True.
+  assert_succeeds (exact I).
+  idtac.
+  (* Error: No such goal. *)
+Abort.
diff --git a/test-suite/ltac2/term_notations.v b/test-suite/ltac2/term_notations.v
new file mode 100644
index 0000000000..85eb858d4e
--- /dev/null
+++ b/test-suite/ltac2/term_notations.v
@@ -0,0 +1,33 @@
+Require Import Ltac2.Ltac2.
+
+(* Preterms are not terms *)
+Fail Notation "[ x ]" := $x.
+
+Section Foo.
+
+Notation "[ x ]" := ltac2:(Control.refine (fun _ => Constr.pretype x)).
+
+Goal [ True ].
+Proof.
+constructor.
+Qed.
+
+End Foo.
+
+Section Bar.
+
+(* Have fun with context capture *)
+Notation "[ x ]" := ltac2:(
+  let c () := Constr.pretype x in
+  refine constr:(forall n : nat, n = ltac2:(Notations.exact0 true c))
+).
+
+Goal forall n : nat, [ n ].
+Proof.
+reflexivity.
+Qed.
+
+(* This fails currently, which is arguably a bug *)
+Fail Goal [ n ].
+
+End Bar.
diff --git a/test-suite/output-coqtop/ShowProofDiffs.out b/test-suite/output-coqtop/ShowProofDiffs.out
new file mode 100644
index 0000000000..285a3bcd89
--- /dev/null
+++ b/test-suite/output-coqtop/ShowProofDiffs.out
@@ -0,0 +1,42 @@
+

+Coq < Coq < 1 subgoal

+  

+  ============================

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

+

+x < 

+x < 1 focused subgoal

+(shelved: 1)

+  i : nat

+  ============================

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

+

+(fun i : nat =>

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

+

+x < 1 focused subgoal

+(shelved: 2)

+  i : nat

+  ============================

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

+

+(fun i : nat =>

+ 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

+(shelved: 2)

+  i : nat

+  ============================

+  i = ?j

+

+subgoal 2 is:

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

+

+(fun i : nat =>

+ 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 (conj ?Goal ?Goal0)))

+

+x < 

diff --git a/test-suite/output-coqtop/ShowProofDiffs.v b/test-suite/output-coqtop/ShowProofDiffs.v
new file mode 100644
index 0000000000..4251c52cb4
--- /dev/null
+++ b/test-suite/output-coqtop/ShowProofDiffs.v
@@ -0,0 +1,6 @@
+(* coq-prog-args: ("-color" "on" "-diffs" "on") *)
+Lemma x: forall(i : nat), exists(j k : nat), i = j /\ j = k /\ i = k.
+Proof using.
+  eexists.  Show Proof Diffs.
+  eexists.  Show Proof Diffs.
+  split.  Show Proof Diffs.
diff --git a/test-suite/output/Arguments.out b/test-suite/output/Arguments.out
index 3c1e27ba9d..6704337f80 100644
--- a/test-suite/output/Arguments.out
+++ b/test-suite/output/Arguments.out
@@ -1,14 +1,14 @@
 Nat.sub : nat -> nat -> nat
 
 Nat.sub is not universe polymorphic
-Argument scopes are [nat_scope nat_scope]
+Arguments Nat.sub _%nat_scope _%nat_scope : simpl nomatch
 The reduction tactics unfold Nat.sub but avoid exposing match constructs
 Nat.sub is transparent
 Expands to: Constant Coq.Init.Nat.sub
 Nat.sub : nat -> nat -> nat
 
 Nat.sub is not universe polymorphic
-Argument scopes are [nat_scope nat_scope]
+Arguments Nat.sub _%nat_scope / _%nat_scope : simpl nomatch
 The reduction tactics unfold Nat.sub when applied to 1 argument
   but avoid exposing match constructs
 Nat.sub is transparent
@@ -16,7 +16,7 @@ Expands to: Constant Coq.Init.Nat.sub
 Nat.sub : nat -> nat -> nat
 
 Nat.sub is not universe polymorphic
-Argument scopes are [nat_scope nat_scope]
+Arguments Nat.sub !_%nat_scope / _%nat_scope : simpl nomatch
 The reduction tactics unfold Nat.sub
   when the 1st argument evaluates to a constructor and
   when applied to 1 argument but avoid exposing match constructs
@@ -25,7 +25,7 @@ Expands to: Constant Coq.Init.Nat.sub
 Nat.sub : nat -> nat -> nat
 
 Nat.sub is not universe polymorphic
-Argument scopes are [nat_scope nat_scope]
+Arguments Nat.sub !_%nat_scope !_%nat_scope /
 The reduction tactics unfold Nat.sub when the 1st and
   2nd arguments evaluate to a constructor and when applied to 2 arguments
 Nat.sub is transparent
@@ -33,7 +33,7 @@ Expands to: Constant Coq.Init.Nat.sub
 Nat.sub : nat -> nat -> nat
 
 Nat.sub is not universe polymorphic
-Argument scopes are [nat_scope nat_scope]
+Arguments Nat.sub !_%nat_scope !_%nat_scope
 The reduction tactics unfold Nat.sub when the 1st and
   2nd arguments evaluate to a constructor
 Nat.sub is transparent
@@ -43,37 +43,34 @@ forall D1 C1 : Type,
 (D1 -> C1) -> forall D2 C2 : Type, (D2 -> C2) -> D1 * D2 -> C1 * C2
 
 pf is not universe polymorphic
-Arguments D2, C2 are implicit
-Arguments D1, C1 are implicit and maximally inserted
-Argument scopes are [foo_scope type_scope _ _ _ _ _]
+Arguments pf {D1%foo_scope} {C1%type_scope} _ [D2] [C2] : simpl never
 The reduction tactics never unfold pf
 pf is transparent
 Expands to: Constant Arguments.pf
 fcomp : forall A B C : Type, (B -> C) -> (A -> B) -> A -> C
 
 fcomp is not universe polymorphic
-Arguments A, B, C are implicit and maximally inserted
-Argument scopes are [type_scope type_scope type_scope _ _ _]
+Arguments fcomp {A%type_scope} {B%type_scope} {C%type_scope} _ _ _ /
 The reduction tactics unfold fcomp when applied to 6 arguments
 fcomp is transparent
 Expands to: Constant Arguments.fcomp
 volatile : nat -> nat
 
 volatile is not universe polymorphic
-Argument scope is [nat_scope]
+Arguments volatile / _%nat_scope
 The reduction tactics always unfold volatile
 volatile is transparent
 Expands to: Constant Arguments.volatile
 f : T1 -> T2 -> nat -> unit -> nat -> nat
 
 f is not universe polymorphic
-Argument scopes are [_ _ nat_scope _ nat_scope]
+Arguments f _ _ _%nat_scope _ _%nat_scope
 f is transparent
 Expands to: Constant Arguments.S1.S2.f
 f : T1 -> T2 -> nat -> unit -> nat -> nat
 
 f is not universe polymorphic
-Argument scopes are [_ _ nat_scope _ nat_scope]
+Arguments f _ _ !_%nat_scope !_ !_%nat_scope
 The reduction tactics unfold f when the 3rd, 4th and
   5th arguments evaluate to a constructor
 f is transparent
@@ -81,8 +78,7 @@ Expands to: Constant Arguments.S1.S2.f
 f : forall T2 : Type, T1 -> T2 -> nat -> unit -> nat -> nat
 
 f is not universe polymorphic
-Argument T2 is implicit
-Argument scopes are [type_scope _ _ nat_scope _ nat_scope]
+Arguments f [T2%type_scope] _ _ !_%nat_scope !_ !_%nat_scope
 The reduction tactics unfold f when the 4th, 5th and
   6th arguments evaluate to a constructor
 f is transparent
@@ -90,8 +86,7 @@ Expands to: Constant Arguments.S1.f
 f : forall T1 T2 : Type, T1 -> T2 -> nat -> unit -> nat -> nat
 
 f is not universe polymorphic
-Arguments T1, T2 are implicit
-Argument scopes are [type_scope type_scope _ _ nat_scope _ nat_scope]
+Arguments f [T1%type_scope] [T2%type_scope] _ _ !_%nat_scope !_ !_%nat_scope
 The reduction tactics unfold f when the 5th, 6th and
   7th arguments evaluate to a constructor
 f is transparent
@@ -103,6 +98,7 @@ Expands to: Constant Arguments.f
 f : forall T1 T2 : Type, T1 -> T2 -> nat -> unit -> nat -> nat
 
 f is not universe polymorphic
+Arguments f _ _ _ _ !_ !_ !_
 The reduction tactics unfold f when the 5th, 6th and
   7th arguments evaluate to a constructor
 f is transparent
@@ -118,7 +114,7 @@ Extra arguments: _, _.
 volatilematch : nat -> nat
 
 volatilematch is not universe polymorphic
-Argument scope is [nat_scope]
+Arguments volatilematch / _%nat_scope : simpl nomatch
 The reduction tactics always unfold volatilematch
   but avoid exposing match constructs
 volatilematch is transparent
diff --git a/test-suite/output/ArgumentsScope.out b/test-suite/output/ArgumentsScope.out
index 69ba329ff1..7b25fd40f8 100644
--- a/test-suite/output/ArgumentsScope.out
+++ b/test-suite/output/ArgumentsScope.out
@@ -1,29 +1,29 @@
 a : bool -> bool
 
 a is not universe polymorphic
-Argument scope is [bool_scope]
+Arguments a _%bool_scope
 Expands to: Variable a
 b : bool -> bool
 
 b is not universe polymorphic
-Argument scope is [bool_scope]
+Arguments b _%bool_scope
 Expands to: Variable b
 negb'' : bool -> bool
 
 negb'' is not universe polymorphic
-Argument scope is [bool_scope]
+Arguments negb'' _%bool_scope
 negb'' is transparent
 Expands to: Constant ArgumentsScope.A.B.negb''
 negb' : bool -> bool
 
 negb' is not universe polymorphic
-Argument scope is [bool_scope]
+Arguments negb' _%bool_scope
 negb' is transparent
 Expands to: Constant ArgumentsScope.A.negb'
 negb : bool -> bool
 
 negb is not universe polymorphic
-Argument scope is [bool_scope]
+Arguments negb _%bool_scope
 negb is transparent
 Expands to: Constant Coq.Init.Datatypes.negb
 a : bool -> bool
diff --git a/test-suite/output/Arguments_renaming.out b/test-suite/output/Arguments_renaming.out
index 65c902202d..53d5624f6f 100644
--- a/test-suite/output/Arguments_renaming.out
+++ b/test-suite/output/Arguments_renaming.out
@@ -13,36 +13,21 @@ where
 ?y : [ |- nat]
 Inductive eq (A : Type) (x : A) : A -> Prop :=  eq_refl : x = x
 
-For eq_refl: Arguments are renamed to B, y
-For eq: Argument A is implicit and maximally inserted
-For eq_refl, when applied to no arguments:
-  Arguments B, y are implicit and maximally inserted
-For eq_refl, when applied to 1 argument:
-  Argument B is implicit
-For eq: Argument scopes are [type_scope _ _]
-For eq_refl: Argument scopes are [type_scope _]
+Arguments eq {A%type_scope}
+Arguments eq_refl {B%type_scope} {y}, [B] _
 eq_refl : forall (A : Type) (x : A), x = x
 
 eq_refl is not universe polymorphic
-Arguments are renamed to B, y
-When applied to no arguments:
-  Arguments B, y are implicit and maximally inserted
-When applied to 1 argument:
-  Argument B is implicit
-Argument scopes are [type_scope _]
+Arguments eq_refl {B%type_scope} {y}, [B] _
 Expands to: Constructor Coq.Init.Logic.eq_refl
 Inductive myEq (B : Type) (x : A) : A -> Prop :=  myrefl : B -> myEq B x x
 
-For myrefl: Arguments are renamed to C, x, _
-For myrefl: Argument C is implicit and maximally inserted
-For myEq: Argument scopes are [type_scope _ _]
-For myrefl: Argument scopes are [type_scope _ _]
+Arguments myEq _%type_scope
+Arguments myrefl {C%type_scope} x : rename
 myrefl : forall (B : Type) (x : A), B -> myEq B x x
 
 myrefl is not universe polymorphic
-Arguments are renamed to C, x, _
-Argument C is implicit and maximally inserted
-Argument scopes are [type_scope _ _]
+Arguments myrefl {C%type_scope} x : rename
 Expands to: Constructor Arguments_renaming.Test1.myrefl
 myplus = 
 fix myplus (T : Type) (t : T) (n m : nat) {struct n} : nat :=
@@ -52,15 +37,11 @@ fix myplus (T : Type) (t : T) (n m : nat) {struct n} : nat :=
   end
      : forall T : Type, T -> nat -> nat -> nat
 
-Arguments are renamed to Z, t, n, m
-Argument Z is implicit and maximally inserted
-Argument scopes are [type_scope _ nat_scope nat_scope]
+Arguments myplus {Z%type_scope} !t !n%nat_scope m%nat_scope : rename
 myplus : forall T : Type, T -> nat -> nat -> nat
 
 myplus is not universe polymorphic
-Arguments are renamed to Z, t, n, m
-Argument Z is implicit and maximally inserted
-Argument scopes are [type_scope _ nat_scope nat_scope]
+Arguments myplus {Z%type_scope} !t !n%nat_scope m%nat_scope : rename
 The reduction tactics unfold myplus when the 2nd and
   3rd arguments evaluate to a constructor
 myplus is transparent
@@ -70,16 +51,12 @@ Expands to: Constant Arguments_renaming.Test1.myplus
 Inductive myEq (A B : Type) (x : A) : A -> Prop :=
     myrefl : B -> myEq A B x x
 
-For myrefl: Arguments are renamed to A, C, x, _
-For myrefl: Argument C is implicit and maximally inserted
-For myEq: Argument scopes are [type_scope type_scope _ _]
-For myrefl: Argument scopes are [type_scope type_scope _ _]
+Arguments myEq _%type_scope _%type_scope
+Arguments myrefl A%type_scope {C%type_scope} x : rename
 myrefl : forall (A B : Type) (x : A), B -> myEq A B x x
 
 myrefl is not universe polymorphic
-Arguments are renamed to A, C, x, _
-Argument C is implicit and maximally inserted
-Argument scopes are [type_scope type_scope _ _]
+Arguments myrefl A%type_scope {C%type_scope} x : rename
 Expands to: Constructor Arguments_renaming.myrefl
 myrefl
      : forall (A C : Type) (x : A), C -> myEq A C x x
@@ -91,15 +68,11 @@ fix myplus (T : Type) (t : T) (n m : nat) {struct n} : nat :=
   end
      : forall T : Type, T -> nat -> nat -> nat
 
-Arguments are renamed to Z, t, n, m
-Argument Z is implicit and maximally inserted
-Argument scopes are [type_scope _ nat_scope nat_scope]
+Arguments myplus {Z%type_scope} !t !n%nat_scope m%nat_scope : rename
 myplus : forall T : Type, T -> nat -> nat -> nat
 
 myplus is not universe polymorphic
-Arguments are renamed to Z, t, n, m
-Argument Z is implicit and maximally inserted
-Argument scopes are [type_scope _ nat_scope nat_scope]
+Arguments myplus {Z%type_scope} !t !n%nat_scope m%nat_scope : rename
 The reduction tactics unfold myplus when the 2nd and
   3rd arguments evaluate to a constructor
 myplus is transparent
diff --git a/test-suite/output/Cases.out b/test-suite/output/Cases.out
index cb835ab48d..7489b8987e 100644
--- a/test-suite/output/Cases.out
+++ b/test-suite/output/Cases.out
@@ -7,7 +7,7 @@ fix F (t : t) : P t :=
      : forall P : t -> Type,
        (let x := t in forall x0 : x, P x0 -> P (k x0)) -> forall t : t, P t
 
-Argument scopes are [function_scope function_scope _]
+Arguments t_rect _%function_scope _%function_scope
      = fun d : TT => match d with
                      | {| f3 := b |} => b
                      end
@@ -26,7 +26,7 @@ match Nat.eq_dec x y with
 end
      : forall (x y : nat) (P : nat -> Type), P x -> P y -> P y
 
-Argument scopes are [nat_scope nat_scope function_scope _ _]
+Arguments proj _%nat_scope _%nat_scope _%function_scope
 foo = 
 fix foo (A : Type) (l : list A) {struct l} : option A :=
   match l with
@@ -36,14 +36,14 @@ fix foo (A : Type) (l : list A) {struct l} : option A :=
   end
      : forall A : Type, list A -> option A
 
-Argument scopes are [type_scope list_scope]
+Arguments foo _%type_scope _%list_scope
 uncast = 
 fun (A : Type) (x : I A) => match x with
                             | x0 <: _ => x0
                             end
      : forall A : Type, I A -> A
 
-Argument scopes are [type_scope _]
+Arguments uncast _%type_scope
 foo' = if A 0 then true else false
      : bool
 f = 
@@ -82,7 +82,7 @@ lem2 =
 fun dd : bool => if dd as aa return (aa = aa) then eq_refl else eq_refl
      : forall k : bool, k = k
 
-Argument scope is [bool_scope]
+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
diff --git a/test-suite/output/Implicit.out b/test-suite/output/Implicit.out
index 3b65003c29..d65d2a8f55 100644
--- a/test-suite/output/Implicit.out
+++ b/test-suite/output/Implicit.out
@@ -5,8 +5,7 @@ ex_intro (P:=fun _ : nat => True) (x:=0) I
 d2 = fun x : nat => d1 (y:=x)
      : forall x x0 : nat, x0 = x -> x0 = x
 
-Arguments x, x0 are implicit
-Argument scopes are [nat_scope nat_scope _]
+Arguments d2 [x%nat_scope] [x0%nat_scope]
 map id (1 :: nil)
      : list nat
 map id' (1 :: nil)
diff --git a/test-suite/output/Inductive.out b/test-suite/output/Inductive.out
index af202ea01c..8ff571ae55 100644
--- a/test-suite/output/Inductive.out
+++ b/test-suite/output/Inductive.out
@@ -3,5 +3,5 @@ Last occurrence of "list'" must have "A" as 1st argument in
  "A -> list' A -> list' (A * A)%type".
 Inductive foo (A : Type) (x : A) (y : A := x) : Prop :=  Foo : foo A x
 
-For foo: Argument scopes are [type_scope _]
-For Foo: Argument scopes are [type_scope _]
+Arguments foo _%type_scope
+Arguments Foo _%type_scope
diff --git a/test-suite/output/InitSyntax.out b/test-suite/output/InitSyntax.out
index c17c63e724..ce058a6d34 100644
--- a/test-suite/output/InitSyntax.out
+++ b/test-suite/output/InitSyntax.out
@@ -1,11 +1,8 @@
 Inductive sig2 (A : Type) (P Q : A -> Prop) : Type :=
     exist2 : forall x : A, P x -> Q x -> {x : A | P x & Q x}
 
-For sig2: Argument A is implicit
-For exist2: Argument A is implicit
-For sig2: Argument scopes are [type_scope type_scope type_scope]
-For exist2: Argument scopes are [type_scope function_scope function_scope _ _
-              _]
+Arguments sig2 [A%type_scope] _%type_scope _%type_scope
+Arguments exist2 [A%type_scope] _%function_scope _%function_scope
 exists x : nat, x = x
      : Prop
 fun b : bool => if b then b else b
diff --git a/test-suite/output/Notations3.out b/test-suite/output/Notations3.out
index d32cf67e28..abada44da7 100644
--- a/test-suite/output/Notations3.out
+++ b/test-suite/output/Notations3.out
@@ -230,7 +230,7 @@ fun l : list nat => match l with
                     end
      : list nat -> list nat
 
-Argument scope is [list_scope]
+Arguments foo _%list_scope
 Notation
 "'exists' x .. y , p" := ex (fun x => .. (ex (fun y => p)) ..) : type_scope
 (default interpretation)
diff --git a/test-suite/output/NumeralNotations.out b/test-suite/output/NumeralNotations.out
index 460c77879c..505dc52ebe 100644
--- a/test-suite/output/NumeralNotations.out
+++ b/test-suite/output/NumeralNotations.out
@@ -180,3 +180,41 @@ let v := 4%Zlike in v : Zlike
      : Zlike
 0%Zlike
      : Zlike
+let v := 0%kt in v : ty
+     : ty
+let v := 1%kt in v : ty
+     : ty
+let v := 2%kt in v : ty
+     : ty
+let v := 3%kt in v : ty
+     : ty
+let v := 4%kt in v : ty
+     : ty
+let v := 5%kt in v : ty
+     : ty
+The command has indeed failed with message:
+Cannot interpret this number as a value of type ty
+     = 0%kt
+     : ty
+     = 1%kt
+     : ty
+     = 2%kt
+     : ty
+     = 3%kt
+     : ty
+     = 4%kt
+     : ty
+     = 5%kt
+     : ty
+let v : ty := Build_ty Empty_set zero in v : ty
+     : ty
+let v : ty := Build_ty unit one in v : ty
+     : ty
+let v : ty := Build_ty bool two in v : ty
+     : ty
+let v : ty := Build_ty Prop prop in v : ty
+     : ty
+let v : ty := Build_ty Set set in v : ty
+     : ty
+let v : ty := Build_ty Type type in v : ty
+     : ty
diff --git a/test-suite/output/NumeralNotations.v b/test-suite/output/NumeralNotations.v
index 44805ad09d..c306b15ef3 100644
--- a/test-suite/output/NumeralNotations.v
+++ b/test-suite/output/NumeralNotations.v
@@ -391,3 +391,68 @@ Module Test19.
   Check {| summands := (cons 1 (cons 2 (cons (-1) nil)))%Z |}.
   Check {| summands := nil |}.
 End Test19.
+
+Module Test20.
+  (** Test Sorts *)
+  Local Set Universe Polymorphism.
+  Inductive known_type : Type -> Type :=
+  | prop : known_type Prop
+  | set : known_type Set
+  | type : known_type Type
+  | zero : known_type Empty_set
+  | one : known_type unit
+  | two : known_type bool.
+
+  Existing Class known_type.
+  Existing Instances zero one two prop.
+  Existing Instance set | 2.
+  Existing Instance type | 4.
+
+  Record > ty := { t : Type ; kt : known_type t }.
+
+  Definition ty_of_uint (x : Decimal.uint) : option ty
+    := match Nat.of_uint x with
+       | 0 => @Some ty zero
+       | 1 => @Some ty one
+       | 2 => @Some ty two
+       | 3 => @Some ty prop
+       | 4 => @Some ty set
+       | 5 => @Some ty type
+       | _ => None
+       end.
+  Definition uint_of_ty (x : ty) : Decimal.uint
+    := Nat.to_uint match kt x with
+                   | prop => 3
+                   | set => 4
+                   | type => 5
+                   | zero => 0
+                   | one => 1
+                   | two => 2
+                   end.
+
+  Declare Scope kt_scope.
+  Delimit Scope kt_scope with kt.
+
+  Numeral Notation ty ty_of_uint uint_of_ty : kt_scope.
+
+  Check let v := 0%kt in v : ty.
+  Check let v := 1%kt in v : ty.
+  Check let v := 2%kt in v : ty.
+  Check let v := 3%kt in v : ty.
+  Check let v := 4%kt in v : ty.
+  Check let v := 5%kt in v : ty.
+  Fail Check let v := 6%kt in v : ty.
+  Eval cbv in (_ : known_type Empty_set) : ty.
+  Eval cbv in (_ : known_type unit) : ty.
+  Eval cbv in (_ : known_type bool) : ty.
+  Eval cbv in (_ : known_type Prop) : ty.
+  Eval cbv in (_ : known_type Set) : ty.
+  Eval cbv in (_ : known_type Type) : ty.
+  Local Set Printing All.
+  Check let v := 0%kt in v : ty.
+  Check let v := 1%kt in v : ty.
+  Check let v := 2%kt in v : ty.
+  Check let v := 3%kt in v : ty.
+  Check let v := 4%kt in v : ty.
+  Check let v := 5%kt in v : ty.
+End Test20.
diff --git a/test-suite/output/PatternsInBinders.out b/test-suite/output/PatternsInBinders.out
index 8a6d94c732..2952b6d94b 100644
--- a/test-suite/output/PatternsInBinders.out
+++ b/test-suite/output/PatternsInBinders.out
@@ -15,8 +15,7 @@ swap =
 fun (A B : Type) '(x, y) => (y, x)
      : forall A B : Type, A * B -> B * A
 
-Arguments A, B are implicit and maximally inserted
-Argument scopes are [type_scope type_scope _]
+Arguments swap {A%type_scope} {B%type_scope}
 fun (A B : Type) '(x, y) => swap (x, y) = (y, x)
      : forall A B : Type, A * B -> Prop
 forall (A B : Type) '(x, y), swap (x, y) = (y, x)
@@ -42,6 +41,6 @@ fun (pat : nat) '(x, y) => x + y = pat
 f = fun x : nat => x + x
      : nat -> nat
 
-Argument scope is [nat_scope]
+Arguments f _%nat_scope
 fun x : nat => x + x
      : nat -> nat
diff --git a/test-suite/output/PrintInfos.out b/test-suite/output/PrintInfos.out
index e788977fb7..7d0d81a3e8 100644
--- a/test-suite/output/PrintInfos.out
+++ b/test-suite/output/PrintInfos.out
@@ -1,36 +1,24 @@
 existT : forall (A : Type) (P : A -> Type) (x : A), P x -> {x : A & P x}
 
 existT is template universe polymorphic on sigT.u0 sigT.u1
-Argument A is implicit
-Argument scopes are [type_scope function_scope _ _]
+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}
 
-For sigT: Argument A is implicit
-For existT: Argument A is implicit
-For sigT: Argument scopes are [type_scope type_scope]
-For existT: Argument scopes are [type_scope function_scope _ _]
+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
 
-For eq: Argument A is implicit and maximally inserted
-For eq_refl, when applied to no arguments:
-  Arguments A, x are implicit and maximally inserted
-For eq_refl, when applied to 1 argument:
-  Argument A is implicit
-For eq: Argument scopes are [type_scope _ _]
-For eq_refl: Argument scopes are [type_scope _]
+Arguments eq {A%type_scope}
+Arguments eq_refl {A%type_scope} {x}, [A] _
 eq_refl : forall (A : Type) (x : A), x = x
 
 eq_refl is not universe polymorphic
-When applied to no arguments:
-  Arguments A, x are implicit and maximally inserted
-When applied to 1 argument:
-  Argument A is implicit
-Argument scopes are [type_scope _]
+Arguments eq_refl {A%type_scope} {x}, [A] _
 Expands to: Constructor Coq.Init.Logic.eq_refl
 eq_refl : forall (A : Type) (x : A), x = x
 
@@ -46,11 +34,11 @@ fix add (n m : nat) {struct n} : nat :=
   end
      : nat -> nat -> nat
 
-Argument scopes are [nat_scope nat_scope]
+Arguments Nat.add _%nat_scope _%nat_scope
 Nat.add : nat -> nat -> nat
 
 Nat.add is not universe polymorphic
-Argument scopes are [nat_scope nat_scope]
+Arguments Nat.add _%nat_scope _%nat_scope
 Nat.add is transparent
 Expands to: Constant Coq.Init.Nat.add
 Nat.add : nat -> nat -> nat
@@ -58,17 +46,15 @@ Nat.add : nat -> nat -> nat
 plus_n_O : forall n : nat, n = n + 0
 
 plus_n_O is not universe polymorphic
-Argument scope is [nat_scope]
+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
 
-For le_S: Argument m is implicit
-For le_S: Argument n is implicit and maximally inserted
-For le: Argument scopes are [nat_scope nat_scope]
-For le_n: Argument scope is [nat_scope]
-For le_S: Argument scopes are [nat_scope nat_scope _]
+Arguments le _%nat_scope _%nat_scope
+Arguments le_n _%nat_scope
+Arguments le_S {n%nat_scope} [m%nat_scope]
 comparison : Set
 
 comparison is not universe polymorphic
@@ -81,26 +67,21 @@ bar is not universe polymorphic
 Expanded type for implicit arguments
 bar : forall x : nat, x = 0
 
-Argument x is implicit and maximally inserted
+Arguments bar {x}
 Expands to: Constant PrintInfos.bar
 *** [ bar : foo ]
 
 Expanded type for implicit arguments
 bar : forall x : nat, x = 0
 
-Argument x is implicit and maximally inserted
+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
 
-For eq: Argument A is implicit and maximally inserted
-For eq_refl, when applied to no arguments:
-  Arguments A, x are implicit and maximally inserted
-For eq_refl, when applied to 1 argument:
-  Argument A is implicit and maximally inserted
-For eq: Argument scopes are [type_scope _ _]
-For eq_refl: Argument scopes are [type_scope _]
+Arguments eq {A%type_scope}
+Arguments eq_refl {A%type_scope} {x}, {A} _
 n:nat
 
 Hypothesis of the goal context.
diff --git a/test-suite/output/StringSyntax.out b/test-suite/output/StringSyntax.out
index 9366113c0c..e9cf4282dc 100644
--- a/test-suite/output/StringSyntax.out
+++ b/test-suite/output/StringSyntax.out
@@ -433,7 +433,7 @@ end
        P "167" ->
        P "168" -> P "169" -> P "170" -> P "171" -> P "172" -> P "173" -> P "174" -> P "175" -> P "176" -> P "177" -> P "178" -> P "179" -> P "180" -> P "181" -> P "182" -> P "183" -> P "184" -> P "185" -> P "186" -> P "187" -> P "188" -> P "189" -> P "190" -> P "191" -> P "192" -> P "193" -> P "194" -> P "195" -> P "196" -> P "197" -> P "198" -> P "199" -> P "200" -> P "201" -> P "202" -> P "203" -> P "204" -> P "205" -> P "206" -> P "207" -> P "208" -> P "209" -> P "210" -> P "211" -> P "212" -> P "213" -> P "214" -> P "215" -> P "216" -> P "217" -> P "218" -> P "219" -> P "220" -> P "221" -> P "222" -> P "223" -> P "224" -> P "225" -> P "226" -> P "227" -> P "228" -> P "229" -> P "230" -> P "231" -> P "232" -> P "233" -> P "234" -> P "235" -> P "236" -> P "237" -> P "238" -> P "239" -> P "240" -> P "241" -> P "242" -> P "243" -> P "244" -> P "245" -> P "246" -> P "247" -> P "248" -> P "249" -> P "250" -> P "251" -> P "252" -> P "253" -> P "254" -> P "255" -> forall b : byte, P b
 
-Argument scopes are [function_scope _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ byte_scope]
+Arguments byte_rect _%function_scope _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _%byte_scope
 byte_rec = 
 fun P : byte -> Set => byte_rect P
      : forall P : byte -> Set,
@@ -607,7 +607,7 @@ fun P : byte -> Set => byte_rect P
        P "167" ->
        P "168" -> P "169" -> P "170" -> P "171" -> P "172" -> P "173" -> P "174" -> P "175" -> P "176" -> P "177" -> P "178" -> P "179" -> P "180" -> P "181" -> P "182" -> P "183" -> P "184" -> P "185" -> P "186" -> P "187" -> P "188" -> P "189" -> P "190" -> P "191" -> P "192" -> P "193" -> P "194" -> P "195" -> P "196" -> P "197" -> P "198" -> P "199" -> P "200" -> P "201" -> P "202" -> P "203" -> P "204" -> P "205" -> P "206" -> P "207" -> P "208" -> P "209" -> P "210" -> P "211" -> P "212" -> P "213" -> P "214" -> P "215" -> P "216" -> P "217" -> P "218" -> P "219" -> P "220" -> P "221" -> P "222" -> P "223" -> P "224" -> P "225" -> P "226" -> P "227" -> P "228" -> P "229" -> P "230" -> P "231" -> P "232" -> P "233" -> P "234" -> P "235" -> P "236" -> P "237" -> P "238" -> P "239" -> P "240" -> P "241" -> P "242" -> P "243" -> P "244" -> P "245" -> P "246" -> P "247" -> P "248" -> P "249" -> P "250" -> P "251" -> P "252" -> P "253" -> P "254" -> P "255" -> forall b : byte, P b
 
-Argument scopes are [function_scope _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ byte_scope]
+Arguments byte_rec _%function_scope _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _%byte_scope
 byte_ind = 
 fun (P : byte -> Prop) (f : P "000") (f0 : P "001") (f1 : P "002") (f2 : P "003") (f3 : P "004") (f4 : P "005") (f5 : P "006") (f6 : P "007") (f7 : P "008") (f8 : P "009") (f9 : P "010") (f10 : P "011") (f11 : P "012") (f12 : P "013") (f13 : P "014") (f14 : P "015") (f15 : P "016") (f16 : P "017") (f17 : P "018") (f18 : P "019") (f19 : P "020") (f20 : P "021") (f21 : P "022") (f22 : P "023") (f23 : P "024") (f24 : P "025") (f25 : P "026") (f26 : P "027") (f27 : P "028") (f28 : P "029") (f29 : P "030") (f30 : P "031") (f31 : P " ") (f32 : P "!") (f33 : P """") (f34 : P "#") (f35 : P "$") (f36 : P "%") (f37 : P "&") (f38 : P "'") (f39 : P "(") (f40 : P ")") (f41 : P "*") (f42 : P "+") (f43 : P ",") (f44 : P "-") (f45 : P ".") (f46 : P "/") (f47 : P "0") (f48 : P "1") (f49 : P "2") (f50 : P "3") (f51 : P "4") (f52 : P "5") (f53 : P "6") (f54 : P "7") (f55 : P "8") (f56 : P "9") (f57 : P ":") (f58 : P ";") (f59 : P "<") (f60 : P "=") (f61 : P ">") (f62 : P "?") 
   (f63 : P "@") (f64 : P "A") (f65 : P "B") (f66 : P "C") (f67 : P "D") (f68 : P "E") (f69 : P "F") (f70 : P "G") (f71 : P "H") (f72 : P "I") (f73 : P "J") (f74 : P "K") (f75 : P "L") (f76 : P "M") (f77 : P "N") (f78 : P "O") (f79 : P "P") (f80 : P "Q") (f81 : P "R") (f82 : P "S") (f83 : P "T") (f84 : P "U") (f85 : P "V") (f86 : P "W") (f87 : P "X") (f88 : P "Y") (f89 : P "Z") (f90 : P "[") (f91 : P "\") (f92 : P "]") (f93 : P "^") (f94 : P "_") (f95 : P "`") (f96 : P "a") (f97 : P "b") (f98 : P "c") (f99 : P "d") (f100 : P "e") (f101 : P "f") (f102 : P "g") (f103 : P "h") (f104 : P "i") (f105 : P "j") (f106 : P "k") (f107 : P "l") (f108 : P "m") (f109 : P "n") (f110 : P "o") (f111 : P "p") (f112 : P "q") (f113 : P "r") (f114 : P "s") (f115 : P "t") (f116 : P "u") (f117 : P "v") (f118 : P "w") (f119 : P "x") (f120 : P "y") (f121 : P "z") (f122 : P "{") (f123 : P "|") (f124 : P "}") (f125 : P "~") (f126 : P "127") (f127 : P "128") (f128 : P "129") (f129 : P "130") 
@@ -1043,7 +1043,7 @@ end
        P "167" ->
        P "168" -> P "169" -> P "170" -> P "171" -> P "172" -> P "173" -> P "174" -> P "175" -> P "176" -> P "177" -> P "178" -> P "179" -> P "180" -> P "181" -> P "182" -> P "183" -> P "184" -> P "185" -> P "186" -> P "187" -> P "188" -> P "189" -> P "190" -> P "191" -> P "192" -> P "193" -> P "194" -> P "195" -> P "196" -> P "197" -> P "198" -> P "199" -> P "200" -> P "201" -> P "202" -> P "203" -> P "204" -> P "205" -> P "206" -> P "207" -> P "208" -> P "209" -> P "210" -> P "211" -> P "212" -> P "213" -> P "214" -> P "215" -> P "216" -> P "217" -> P "218" -> P "219" -> P "220" -> P "221" -> P "222" -> P "223" -> P "224" -> P "225" -> P "226" -> P "227" -> P "228" -> P "229" -> P "230" -> P "231" -> P "232" -> P "233" -> P "234" -> P "235" -> P "236" -> P "237" -> P "238" -> P "239" -> P "240" -> P "241" -> P "242" -> P "243" -> P "244" -> P "245" -> P "246" -> P "247" -> P "248" -> P "249" -> P "250" -> P "251" -> P "252" -> P "253" -> P "254" -> P "255" -> forall b : byte, P b
 
-Argument scopes are [function_scope _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ byte_scope]
+Arguments byte_ind _%function_scope _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _%byte_scope
 "000"
      : byte
 "a"
diff --git a/test-suite/output/Tactics.out b/test-suite/output/Tactics.out
index 19c9fc4423..70427220ed 100644
--- a/test-suite/output/Tactics.out
+++ b/test-suite/output/Tactics.out
@@ -6,3 +6,4 @@ The command has indeed failed with message:
 H is already used.
 The command has indeed failed with message:
 H is already used.
+a
diff --git a/test-suite/output/Tactics.v b/test-suite/output/Tactics.v
index fa12f09a46..96b6d652c9 100644
--- a/test-suite/output/Tactics.v
+++ b/test-suite/output/Tactics.v
@@ -22,3 +22,11 @@ intros H.
 Fail intros [H%myid ?].
 Fail destruct 1 as [H%myid ?].
 Abort.
+
+
+(* Test that assert_succeeds only runs a tactic once *)
+Ltac should_not_loop := idtac + should_not_loop.
+Goal True.
+  assert_succeeds should_not_loop.
+  assert_succeeds (idtac "a" + idtac "b"). (* should only output "a" *)
+Abort.
diff --git a/test-suite/output/UnivBinders.out b/test-suite/output/UnivBinders.out
index d48d8b900f..298a0789c4 100644
--- a/test-suite/output/UnivBinders.out
+++ b/test-suite/output/UnivBinders.out
@@ -4,37 +4,36 @@ Record PWrap (A : Type@{u}) : Type@{u} := pwrap { punwrap : A }
 (* u |=  *)
 
 PWrap has primitive projections with eta conversion.
-For PWrap: Argument scope is [type_scope]
-For pwrap: Argument scopes are [type_scope _]
+Arguments PWrap _%type_scope
+Arguments pwrap _%type_scope
 punwrap@{u} = 
 fun (A : Type@{u}) (p : PWrap@{u} A) => punwrap _ p
      : forall A : Type@{u}, PWrap@{u} A -> A
 (* u |=  *)
 
-Argument scopes are [type_scope _]
+Arguments punwrap _%type_scope
 Record RWrap (A : Type@{u}) : Type@{u} := rwrap { runwrap : A }
 (* u |=  *)
 
-For RWrap: Argument scope is [type_scope]
-For rwrap: Argument scopes are [type_scope _]
+Arguments RWrap _%type_scope
+Arguments rwrap _%type_scope
 runwrap@{u} = 
 fun (A : Type@{u}) (r : RWrap@{u} A) => let (runwrap) := r in runwrap
      : forall A : Type@{u}, RWrap@{u} A -> A
 (* u |=  *)
 
-Argument scopes are [type_scope _]
+Arguments runwrap _%type_scope
 Wrap@{u} = fun A : Type@{u} => A
      : Type@{u} -> Type@{u}
 (* u |=  *)
 
-Argument scope is [type_scope]
+Arguments Wrap _%type_scope
 wrap@{u} = 
 fun (A : Type@{u}) (Wrap : Wrap@{u} A) => Wrap
      : forall A : Type@{u}, Wrap@{u} A -> A
 (* u |=  *)
 
-Arguments A, Wrap are implicit and maximally inserted
-Argument scopes are [type_scope _]
+Arguments wrap {A%type_scope} {Wrap}
 bar@{u} = nat
      : Wrap@{u} Set
 (* u |= Set < u *)
@@ -87,13 +86,13 @@ Record PWrap (A : Type@{E}) : Type@{E} := pwrap { punwrap : A }
 (* E |=  *)
 
 PWrap has primitive projections with eta conversion.
-For PWrap: Argument scope is [type_scope]
-For pwrap: Argument scopes are [type_scope _]
+Arguments PWrap _%type_scope
+Arguments pwrap _%type_scope
 punwrap@{K} : forall A : Type@{K}, PWrap@{K} A -> A
 (* K |=  *)
 
 punwrap is universe polymorphic
-Argument scopes are [type_scope _]
+Arguments punwrap _%type_scope
 punwrap is transparent
 Expands to: Constant UnivBinders.punwrap
 The command has indeed failed with message:
@@ -118,7 +117,7 @@ Inductive insecind@{k} : Type@{k+1} :=
     inseccstr : Type@{k} -> insecind@{k}
 (* k |=  *)
 
-For inseccstr: Argument scope is [type_scope]
+Arguments inseccstr _%type_scope
 insec@{u v} = Type@{u} -> Type@{v}
      : Type@{max(u+1,v+1)}
 (* u v |=  *)
@@ -126,7 +125,7 @@ Inductive insecind@{u k} : Type@{k+1} :=
     inseccstr : Type@{k} -> insecind@{u k}
 (* u k |=  *)
 
-For inseccstr: Argument scope is [type_scope]
+Arguments inseccstr _%type_scope
 insec2@{u} = Prop
      : Type@{Set+1}
 (* u |=  *)
@@ -148,24 +147,24 @@ Type@{UnivBinders.59} -> Type@{i}
 (* i UnivBinders.59 UnivBinders.60 |=  *)
 
 axfoo is universe polymorphic
-Argument scope is [type_scope]
+Arguments axfoo _%type_scope
 Expands to: Constant UnivBinders.axfoo
 axbar@{i UnivBinders.59 UnivBinders.60} :
 Type@{UnivBinders.60} -> Type@{i}
 (* i UnivBinders.59 UnivBinders.60 |=  *)
 
 axbar is universe polymorphic
-Argument scope is [type_scope]
+Arguments axbar _%type_scope
 Expands to: Constant UnivBinders.axbar
 axfoo' : Type@{axfoo'.u0} -> Type@{axfoo'.i}
 
 axfoo' is not universe polymorphic
-Argument scope is [type_scope]
+Arguments axfoo' _%type_scope
 Expands to: Constant UnivBinders.axfoo'
 axbar' : Type@{axfoo'.u0} -> Type@{axfoo'.i}
 
 axbar' is not universe polymorphic
-Argument scope is [type_scope]
+Arguments axbar' _%type_scope
 Expands to: Constant UnivBinders.axbar'
 The command has indeed failed with message:
 When declaring multiple axioms in one command, only the first is allowed a universe binder (which will be shared by the whole block).
diff --git a/test-suite/success/Fixpoint.v b/test-suite/success/Fixpoint.v
index 81c9763ccd..6c333121da 100644
--- a/test-suite/success/Fixpoint.v
+++ b/test-suite/success/Fixpoint.v
@@ -96,10 +96,25 @@ Section visibility.
 
   Let Fixpoint by_proof (n:nat) : True.
   Proof. exact I. Defined.
+
+  Let Fixpoint foo (n:nat) : bool with bar (n:nat) : bool.
+  Proof.
+    - destruct n as [|n].
+      + exact true.
+      + exact (bar n).
+    - destruct n as [|n].
+      + exact false.
+      + exact (foo n).
+  Qed.
+
+  Let Fixpoint bla (n:nat) : Type with bli (n:nat) : bool.
+  Admitted.
+
 End visibility.
 
 Fail Check imm.
 Fail Check by_proof.
+Check bla. Check bli.
 
 Module Import mod_local.
   Fixpoint imm_importable (n:nat) : True := I.