15 files changed, 598 insertions, 31 deletions
diff --git a/test-suite/output/Cases.out b/test-suite/output/Cases.out
index 97fa8e254..419dcadb4 100644
--- a/test-suite/output/Cases.out
+++ b/test-suite/output/Cases.out
@@ -95,8 +95,7 @@ fun dd : nat * nat => let (bb, cc) as aa return (aa = aa) := dd in eq_refl
   
   x : nat
   n, n0 := match x + 0 with
-           | 0 => 0
-           | S _ => 0
+           | 0 | S _ => 0
            end : nat
   e,
   e0 := match x + 0 as y return (y = y) with
@@ -104,8 +103,7 @@ fun dd : nat * nat => let (bb, cc) as aa return (aa = aa) := dd in eq_refl
         | S n => eq_refl
         end : x + 0 = x + 0
   n1, n2 := match x with
-            | 0 => 0
-            | S _ => 0
+            | 0 | S _ => 0
             end : nat
   e1, e2 := match x return (x = x) with
             | 0 => eq_refl
@@ -126,3 +124,48 @@ fun dd : nat * nat => let (bb, cc) as aa return (aa = aa) := dd in eq_refl
         end : p = p /\ p = p
   ============================
   eq_refl = eq_refl
+fun x : comparison => match x with
+                      | Eq => 1
+                      | _ => 0
+                      end
+     : comparison -> nat
+fun x : comparison => match x with
+                      | Eq => 1
+                      | Lt => 0
+                      | Gt => 0
+                      end
+     : comparison -> nat
+fun x : comparison => match x with
+                      | Eq => 1
+                      | Lt | Gt => 0
+                      end
+     : comparison -> nat
+fun x : comparison =>
+match x return nat with
+| Eq => S O
+| Lt => O
+| Gt => O
+end
+     : forall _ : comparison, nat
+fun x : K => match x with
+             | a3 | a4 => 3
+             | _ => 2
+             end
+     : K -> nat
+fun x : K => match x with
+             | a1 | a2 => 4
+             | a3 => 3
+             | _ => 2
+             end
+     : K -> nat
+fun x : K => match x with
+             | a1 | a2 => 4
+             | a4 => 3
+             | _ => 2
+             end
+     : K -> nat
+fun x : K => match x with
+             | a1 | a3 | a4 => 3
+             | _ => 2
+             end
+     : K -> nat
diff --git a/test-suite/output/Cases.v b/test-suite/output/Cases.v
index 17fee3303..caf3b2870 100644
--- a/test-suite/output/Cases.v
+++ b/test-suite/output/Cases.v
@@ -1,5 +1,7 @@
 (* Cases with let-in in constructors types *)
 
+Unset Printing Allow Match Default Clause.
+
 Inductive t : Set :=
     k : let x := t in x -> x.
 
@@ -184,3 +186,33 @@ let p := fresh "p" in
   |- eq_refl ?p = _ => pose (match eq_refl p in _ = z return p=p /\ z=z with eq_refl => conj eq_refl eq_refl end)
   end.
 Show.
+
+Set Printing Allow Match Default Clause.
+
+(***************************************************)
+(* Testing strategy for factorizing cases branches *)
+
+(* Factorization + default clause *)
+Check fun x => match x with Eq => 1 | _ => 0 end.
+
+(* No factorization *)
+Unset Printing Factorizable Match Patterns.
+Check fun x => match x with Eq => 1 | _ => 0 end.
+Set Printing Factorizable Match Patterns.
+
+(* Factorization but no default clause *)
+Unset Printing Allow Match Default Clause.
+Check fun x => match x with Eq => 1 | _ => 0 end.
+Set Printing Allow Match Default Clause.
+
+(* No factorization in printing all mode *)
+Set Printing All.
+Check fun x => match x with Eq => 1 | _ => 0 end.
+Unset Printing All.
+
+(* Several clauses *)
+Inductive K := a1|a2|a3|a4|a5|a6.
+Check fun x => match x with a3 | a4 => 3 | _ => 2 end.
+Check fun x => match x with a3 => 3 | a2 | a1 => 4 | _ => 2 end.
+Check fun x => match x with a4 => 3 | a2 | a1 => 4 | _ => 2 end.
+Check fun x => match x with a3 | a4 | a1 => 3 | _ => 2 end.
diff --git a/test-suite/output/Extraction_infix.out b/test-suite/output/Extraction_infix.out
new file mode 100644
index 000000000..29d50775a
--- /dev/null
+++ b/test-suite/output/Extraction_infix.out
@@ -0,0 +1,20 @@
+(** val test : foo **)
+
+let test =
+  (fun (b, p) -> bar) (True, False)
+(** val test : foo **)
+
+let test =
+  True@@?False
+(** val test : foo **)
+
+let test =
+  True#^^False
+(** val test : foo **)
+
+let test =
+  True@?:::False
+(** val test : foo **)
+
+let test =
+  True  @?:::  False
diff --git a/test-suite/output/Extraction_infix.v b/test-suite/output/Extraction_infix.v
new file mode 100644
index 000000000..fe5926a36
--- /dev/null
+++ b/test-suite/output/Extraction_infix.v
@@ -0,0 +1,26 @@
+(* @herbelin's example for issue #6212 *)
+
+Require Import Extraction.
+Inductive I := C : bool -> bool -> I.
+Definition test := C true false.
+
+(* the parentheses around the function wrong signalled an infix operator *)
+
+Extract Inductive I => "foo" [ "(fun (b, p) -> bar)" ].
+Extraction test.
+
+(* some bonafide infix operators *)
+
+Extract Inductive I => "foo" [ "(@@?)" ].
+Extraction test.
+
+Extract Inductive I => "foo" [ "(#^^)" ].
+Extraction test.
+
+Extract Inductive I => "foo" [ "(@?:::)" ].
+Extraction test.
+
+(* allow whitespace around infix operator *)
+
+Extract Inductive I => "foo" [ "(  @?:::  )" ].
+Extraction test.
diff --git a/test-suite/output/Notations.out b/test-suite/output/Notations.out
index 7bcd7b041..2f0ee765d 100644
--- a/test-suite/output/Notations.out
+++ b/test-suite/output/Notations.out
@@ -64,7 +64,7 @@ The command has indeed failed with message:
 Cannot find where the recursive pattern starts.
 The command has indeed failed with message:
 Both ends of the recursive pattern are the same.
-SUM (nat * nat) nat
+(nat * nat + nat)%type
      : Set
 FST (0; 1)
      : Z
@@ -72,7 +72,7 @@ Nil
      : forall A : Type, list A
 NIL : list nat
      : list nat
-(false && I 3)%bool /\ I 6
+(false && I 3)%bool /\ (I 6)%bool
      : Prop
 [|1, 2, 3; 4, 5, 6|]
      : Z * Z * Z * (Z * Z * Z)
diff --git a/test-suite/output/Notations.v b/test-suite/output/Notations.v
index fe6c05c39..413812ee1 100644
--- a/test-suite/output/Notations.v
+++ b/test-suite/output/Notations.v
@@ -30,7 +30,7 @@ Check (decomp (true,true) as t, u in (t,u)).
 
 Section A.
 
-Notation "! A" := (forall _:nat, A) (at level 60).
+Notation "! A" := (forall _:nat, A) (at level 60) : type_scope.
 
 Check ! (0=0).
 Check forall n, n=0.
@@ -194,9 +194,9 @@ Open Scope nat_scope.
 
 Coercion is_true := fun b => b=true.
 Coercion of_nat n := match n with 0 => true | _ => false end.
-Notation "'I' x" := (of_nat (S x) || true)%bool (at level 10).
+Notation "'I' x" := (of_nat (S x) || true)%bool (at level 10) : bool_scope.
 
-Check (false && I 3)%bool /\ I 6.
+Check (false && I 3)%bool /\ (I 6)%bool.
 
 (**********************************************************************)
 (* Check notations with several recursive patterns                    *)
diff --git a/test-suite/output/Notations2.out b/test-suite/output/Notations2.out
index 1ec701ae8..121a369a9 100644
--- a/test-suite/output/Notations2.out
+++ b/test-suite/output/Notations2.out
@@ -37,11 +37,22 @@ let' f (x y : nat) (a := 0) (z : nat) (_ : bool) := x + y + z + 1 in f 0 1 2
 λ (f : nat -> nat) (x : nat), f(x) + S(x)
      : (nat -> nat) -> nat -> nat
 Notation plus2 n := (S(S(n)))
+λ n : list(nat), match n with
+                 | 1 :: nil => 0
+                 | _ => 2
+                 end
+     : list(nat) -> nat
+λ n : list(nat),
+match n with
+| 1 :: nil => 0
+| nil | 0 :: _ | 1 :: _ :: _ | plus2 _ :: _ => 2
+end
+     : list(nat) -> nat
 λ n : list(nat),
 match n with
 | nil => 2
 | 0 :: _ => 2
-| list1 => 0
+| 1 :: nil => 0
 | 1 :: _ :: _ => 2
 | plus2 _ :: _ => 2
 end
@@ -84,3 +95,9 @@ a≡
      : Set
 .α
      : Set
+# a : .α =>
+# b : .α =>
+let res := 0 in
+for i from 0 to a updating (res)
+{{for j from 0 to b updating (res) {{S res}};; res}};; res
+     : .α -> .α -> .α
diff --git a/test-suite/output/Notations2.v b/test-suite/output/Notations2.v
index ceb29d1b9..531398bb0 100644
--- a/test-suite/output/Notations2.v
+++ b/test-suite/output/Notations2.v
@@ -70,6 +70,7 @@ Check let' f x y (a:=0) z (b:bool) := x+y+z+1 in f 0 1 2.
 (* Note: does not work for pattern *)
 Module A.
 Notation "f ( x )" := (f x) (at level 10, format "f ( x )").
+Open Scope nat_scope.
 Check fun f x => f x + S x.
 
 Open Scope list_scope.
@@ -78,6 +79,13 @@ Notation plus2 n := (S (S n)).
 (* plus2 was not correctly printed in the two following tests in 8.3pl1 *)
 Print plus2.
 Check fun n => match n with list1 => 0 | _ => 2 end.
+Unset Printing Allow Match Default Clause.
+Check fun n => match n with list1 => 0 | _ => 2 end.
+Unset Printing Factorizable Match Patterns.
+Check fun n => match n with list1 => 0 | _ => 2 end.
+Set Printing Allow Match Default Clause.
+Set Printing Factorizable Match Patterns.
+
 End A.
 
 (* This one is not fully satisfactory because binders in the same type
@@ -145,3 +153,24 @@ Check .a≡.
 Notation ".α" := nat.
 Check nat.
 Check .α.
+
+(* A test for #6304 *)
+
+Module M6304.
+Notation "'for' m 'from' 0 'to' N 'updating' ( s1 )  {{ b }} ;; rest" :=
+  (let s1 :=
+    (fix rec(n: nat) := match n with
+     | 0 => s1
+     | S m => let s1 := rec m in b
+     end) N
+  in rest)
+  (at level 20).
+
+Check fun (a b : nat) =>
+  let res := 0 in
+  for i from 0 to a updating (res) {{
+    for j from 0 to b updating (res) {{ S res }};;
+    res
+  }};; res.
+
+End M6304.
diff --git a/test-suite/output/Notations3.out b/test-suite/output/Notations3.out
index 6ef75dd13..1b5725275 100644
--- a/test-suite/output/Notations3.out
+++ b/test-suite/output/Notations3.out
@@ -128,3 +128,13 @@ return (1, 2, 3, 4)
      : nat
 *(1.2)
      : nat
+[{0; 0}]
+     : list (list nat)
+[{1; 2; 3};
+ {4; 5; 6};
+ {7; 8; 9}]
+     : list (list nat)
+amatch = mmatch 0 (with 0 => 1| 1 => 2 end)
+     : unit
+alist = [0; 1; 2]
+     : list nat
diff --git a/test-suite/output/Notations3.v b/test-suite/output/Notations3.v
index 8c7bbe591..a8d6c97fb 100644
--- a/test-suite/output/Notations3.v
+++ b/test-suite/output/Notations3.v
@@ -59,7 +59,7 @@ Check fun f => CURRYINVLEFT (x:nat) (y:bool), f.
 (* Notations with variables bound both as a term and as a binder      *)
 (* This is #4592 *)
 
-Notation "{# x | P }" := (ex2 (fun y => x = y) (fun x => P)).
+Notation "{# x | P }" := (ex2 (fun y => x = y) (fun x => P)) : type_scope.
 Check forall n:nat, {# n | 1 > n}.
 
 Parameter foo : forall {T}(x : T)(P : T -> Prop), Prop.
@@ -183,9 +183,13 @@ Check letpair x [1] = {0}; return (1,2,3,4).
 
 (* Test spacing in #5569 *)
 
+Section S1.
+Variable plus : nat -> nat -> nat.
+Infix "+" := plus.
 Notation "{ { xL | xR // xcut } }" := (xL+xR+xcut)
   (at level 0, xR at level 39, format "{ {  xL  |  xR  //  xcut  } }").
 Check 1+1+1.
+End S1.
 
 (* Test presence of notation variables in the recursive parts (introduced in dfdaf4de) *)
 Notation "!!! x .. y , b" := ((fun x => b), .. ((fun y => b), True) ..) (at level 200, x binder).
@@ -193,7 +197,59 @@ Check !!! (x y:nat), True.
 
 (* Allow level for leftmost nonterminal when printing-only, BZ#5739 *)
 
-Notation "* x" := (id x) (only printing, at level 15, format "* x").
-Notation "x . y" := (x + y) (only printing, at level 20, x at level 14, left associativity, format "x . y").
+Section S2.
+Notation "* x" := (id x) (only printing, at level 15, format "* x") : nat_scope.
+Notation "x . y" := (x + y) (only printing, at level 20, x at level 14, left associativity, format "x . y") : nat_scope.
 Check (((id 1) + 2) + 3).
 Check (id (1 + 2)).
+End S2.
+
+(* Test printing of notations guided by scope *)
+
+Module A.
+
+Delimit Scope line_scope with line.
+Notation "{ }" := nil (format "{ }") : line_scope.
+Notation "{ x }" := (cons x nil) : line_scope.
+Notation "{ x ; y ; .. ; z }" :=  (cons x (cons y .. (cons z nil) ..)) : line_scope.
+Notation "[ ]" := nil (format "[ ]") : matx_scope.
+Notation "[ l ]" := (cons l%line nil) : matx_scope.
+Notation "[ l ; l' ; .. ; l'' ]" :=  (cons l%line (cons l'%line .. (cons l''%line nil) ..))
+  (format "[ '[v' l ; '/' l' ; '/' .. ; '/' l'' ']' ]") : matx_scope.
+
+Open Scope matx_scope.
+Check [[0;0]].
+Check [[1;2;3];[4;5;6];[7;8;9]].
+
+End A.
+
+(* Example by Beta Ziliani *)
+
+Require Import Lists.List.
+
+Module B.
+
+Import ListNotations.
+
+Delimit Scope pattern_scope with pattern.
+Delimit Scope patterns_scope with patterns.
+
+Notation "a => b" := (a, b) (at level 201) : pattern_scope.
+Notation "'with' p1 | .. | pn 'end'" :=
+  ((cons p1%pattern (.. (cons pn%pattern nil) ..)))
+    (at level 91, p1 at level 210, pn at level 210) : patterns_scope.
+
+Definition mymatch (n:nat) (l : list (nat * nat)) := tt.
+Arguments mymatch _ _%patterns.
+Notation "'mmatch' n ls" := (mymatch n ls) (at level 0).
+
+Close Scope patterns_scope.
+Close Scope pattern_scope.
+
+Definition amatch := mmatch 0 with 0 => 1 | 1 => 2 end.
+Print amatch. (* Good: amatch = mmatch 0 (with 0 => 1| 1 => 2 end) *)
+
+Definition alist := [0;1;2].
+Print alist.
+
+End B.
diff --git a/test-suite/output/UnivBinders.out b/test-suite/output/UnivBinders.out
index 904ff68aa..d6d410d1a 100644
--- a/test-suite/output/UnivBinders.out
+++ b/test-suite/output/UnivBinders.out
@@ -1,12 +1,175 @@
+NonCumulative Inductive Empty@{u} : Type@{u} :=  
+NonCumulative Record PWrap (A : Type@{u}) : Type@{u} := pwrap { punwrap : A }
+
+PWrap has primitive projections with eta conversion.
+For PWrap: Argument scope is [type_scope]
+For pwrap: Argument scopes are [type_scope _]
+punwrap@{u} = 
+fun (A : Type@{u}) (p : PWrap@{u} A) => punwrap _ p
+     : forall A : Type@{u}, PWrap@{u} A -> A
+(* u |=  *)
+
+punwrap is universe polymorphic
+Argument scopes are [type_scope _]
+NonCumulative Record RWrap (A : Type@{u}) : Type@{u} := rwrap { runwrap : A }
+
+For RWrap: Argument scope is [type_scope]
+For rwrap: Argument scopes are [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 |=  *)
+
+runwrap is universe polymorphic
+Argument scopes are [type_scope _]
+Wrap@{u} = fun A : Type@{u} => A
+     : Type@{u} -> Type@{u}
+(* u |=  *)
+
+Wrap is universe polymorphic
+Argument scope is [type_scope]
+wrap@{u} = 
+fun (A : Type@{u}) (Wrap : Wrap@{u} A) => Wrap
+     : forall A : Type@{u}, Wrap@{u} A -> A
+(* u |=  *)
+
+wrap is universe polymorphic
+Arguments A, Wrap are implicit and maximally inserted
+Argument scopes are [type_scope _]
 bar@{u} = nat
      : Wrap@{u} Set
 (* u |= Set < u
          *)
 
 bar is universe polymorphic
-foo@{u Top.8 v} = 
-Type@{Top.8} -> Type@{v} -> Type@{u}
-     : Type@{max(u+1, Top.8+1, v+1)}
-(* u Top.8 v |=  *)
+foo@{u Top.17 v} = 
+Type@{Top.17} -> Type@{v} -> Type@{u}
+     : Type@{max(u+1,Top.17+1,v+1)}
+(* u Top.17 v |=  *)
 
 foo is universe polymorphic
+Monomorphic mono = Type@{mono.u}
+     : Type@{mono.u+1}
+(* {mono.u} |=  *)
+
+mono is not universe polymorphic
+mono
+     : Type@{mono.u+1}
+Type@{mono.u}
+     : Type@{mono.u+1}
+The command has indeed failed with message:
+Universe u already exists.
+monomono
+     : Type@{MONOU+1}
+mono.monomono
+     : Type@{mono.MONOU+1}
+monomono
+     : Type@{MONOU+1}
+mono
+     : Type@{mono.u+1}
+The command has indeed failed with message:
+Universe u already exists.
+bobmorane = 
+let tt := Type@{tt.v} in let ff := Type@{ff.v} in tt -> ff
+     : Type@{max(tt.u,ff.u)}
+The command has indeed failed with message:
+Universe u already bound.
+foo@{E M N} = 
+Type@{M} -> Type@{N} -> Type@{E}
+     : Type@{max(E+1,M+1,N+1)}
+(* E M N |=  *)
+
+foo is universe polymorphic
+foo@{Top.16 Top.17 Top.18} = 
+Type@{Top.17} -> Type@{Top.18} -> Type@{Top.16}
+     : Type@{max(Top.16+1,Top.17+1,Top.18+1)}
+(* Top.16 Top.17 Top.18 |=  *)
+
+foo is universe polymorphic
+NonCumulative Inductive Empty@{E} : Type@{E} :=  
+NonCumulative Record PWrap (A : Type@{E}) : Type@{E} := pwrap { punwrap : A }
+
+PWrap has primitive projections with eta conversion.
+For PWrap: Argument scope is [type_scope]
+For pwrap: Argument scopes are [type_scope _]
+punwrap@{K} : forall A : Type@{K}, PWrap@{K} A -> A
+(* K |=  *)
+
+punwrap is universe polymorphic
+Argument scopes are [type_scope _]
+punwrap is transparent
+Expands to: Constant Top.punwrap
+The command has indeed failed with message:
+Universe instance should have length 3
+The command has indeed failed with message:
+Universe instance should have length 0
+The command has indeed failed with message:
+This object does not support universe names.
+The command has indeed failed with message:
+Cannot enforce v < u because u < gU < gV < v
+Monomorphic bind_univs.mono = 
+Type@{bind_univs.mono.u}
+     : Type@{bind_univs.mono.u+1}
+(* {bind_univs.mono.u} |=  *)
+
+bind_univs.mono is not universe polymorphic
+bind_univs.poly@{u} = Type@{u}
+     : Type@{u+1}
+(* u |=  *)
+
+bind_univs.poly is universe polymorphic
+insec@{v} = Type@{u} -> Type@{v}
+     : Type@{max(u+1,v+1)}
+(* v |=  *)
+
+insec is universe polymorphic
+insec@{u v} = Type@{u} -> Type@{v}
+     : Type@{max(u+1,v+1)}
+(* u v |=  *)
+
+insec is universe polymorphic
+inmod@{u} = Type@{u}
+     : Type@{u+1}
+(* u |=  *)
+
+inmod is universe polymorphic
+SomeMod.inmod@{u} = Type@{u}
+     : Type@{u+1}
+(* u |=  *)
+
+SomeMod.inmod is universe polymorphic
+inmod@{u} = Type@{u}
+     : Type@{u+1}
+(* u |=  *)
+
+inmod is universe polymorphic
+Applied.infunct@{u v} = 
+inmod@{u} -> Type@{v}
+     : Type@{max(u+1,v+1)}
+(* u v |=  *)
+
+Applied.infunct is universe polymorphic
+axfoo@{i Top.41 Top.42} : Type@{Top.41} -> Type@{i}
+(* i Top.41 Top.42 |=  *)
+
+axfoo is universe polymorphic
+Argument scope is [type_scope]
+Expands to: Constant Top.axfoo
+axbar@{i Top.41 Top.42} : Type@{Top.42} -> Type@{i}
+(* i Top.41 Top.42 |=  *)
+
+axbar is universe polymorphic
+Argument scope is [type_scope]
+Expands to: Constant Top.axbar
+axfoo' : Type@{Top.44} -> Type@{axbar'.i}
+
+axfoo' is not universe polymorphic
+Argument scope is [type_scope]
+Expands to: Constant Top.axfoo'
+axbar' : Type@{Top.44} -> Type@{axbar'.i}
+
+axbar' is not universe polymorphic
+Argument scope is [type_scope]
+Expands to: Constant Top.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/output/UnivBinders.v b/test-suite/output/UnivBinders.v
index 8656ff1a3..266d94ad9 100644
--- a/test-suite/output/UnivBinders.v
+++ b/test-suite/output/UnivBinders.v
@@ -1,13 +1,146 @@
 Set Universe Polymorphism.
 Set Printing Universes.
-Unset Strict Universe Declaration.
+(* Unset Strict Universe Declaration. *)
+
+(* universe binders on inductive types and record projections *)
+Inductive Empty@{u} : Type@{u} := .
+Print Empty.
+
+Set Primitive Projections.
+Record PWrap@{u} (A:Type@{u}) := pwrap { punwrap : A }.
+Print PWrap.
+Print punwrap.
+
+Unset Primitive Projections.
+Record RWrap@{u} (A:Type@{u}) := rwrap { runwrap : A }.
+Print RWrap.
+Print runwrap.
 
-Class Wrap A := wrap : A.
+(* universe binders also go on the constants for operational typeclasses. *)
+Class Wrap@{u} (A:Type@{u}) := wrap : A.
+Print Wrap.
+Print wrap.
 
-Instance bar@{u} : Wrap@{u} Set. Proof nat.
+(* Instance in lemma mode used to ignore the binders. *)
+Instance bar@{u} : Wrap@{u} Set. Proof. exact nat. Qed.
 Print bar.
 
+Unset Strict Universe Declaration.
 (* The universes in the binder come first, then the extra universes in
    order of appearance. *)
 Definition foo@{u +} := Type -> Type@{v} -> Type@{u}.
 Print foo.
+Set Strict Universe Declaration.
+
+(* Binders even work with monomorphic definitions! *)
+Monomorphic Definition mono@{u} := Type@{u}.
+Print mono.
+Check mono.
+Check Type@{mono.u}.
+
+Module mono.
+  Fail Monomorphic Universe u.
+  Monomorphic Universe MONOU.
+
+  Monomorphic Definition monomono := Type@{MONOU}.
+  Check monomono.
+End mono.
+Check mono.monomono. (* qualified MONOU *)
+Import mono.
+Check monomono. (* unqualified MONOU *)
+Check mono. (* still qualified mono.u *)
+
+Monomorphic Constraint Set < Top.mono.u.
+
+Module mono2.
+  Monomorphic Universe u.
+End mono2.
+
+Fail Monomorphic Definition mono2@{u} := Type@{u}.
+
+Module SecLet.
+  Unset Universe Polymorphism.
+  Section foo.
+    (* Fail Let foo@{} := Type@{u}. (* doesn't parse: Let foo@{...} doesn't exist *) *)
+    Unset Strict Universe Declaration.
+    Let tt : Type@{u} := Type@{v}. (* names disappear in the ether *)
+    Let ff : Type@{u}. Proof. exact Type@{v}. Qed. (* if Set Universe Polymorphism: universes are named ff.u and ff.v. Otherwise names disappear into space *)
+    Definition bobmorane := tt -> ff.
+  End foo.
+  Print bobmorane. (*
+                     bobmorane@{Top.15 Top.16 ff.u ff.v} =
+                     let tt := Type@{Top.16} in let ff := Type@{ff.v} in tt -> ff
+                     : Type@{max(Top.15,ff.u)}
+                     (* Top.15 Top.16 ff.u ff.v |= Top.16 < Top.15
+                     ff.v < ff.u
+                    *)
+
+                    bobmorane is universe polymorphic
+                    *)
+End SecLet.
+
+(* fun x x => foo is nonsense with local binders *)
+Fail Definition fo@{u u} := Type@{u}.
+
+(* Using local binders for printing. *)
+Print foo@{E M N}.
+(* Underscores discard the name if there's one. *)
+Print foo@{_ _ _}.
+
+(* Also works for inductives and records. *)
+Print Empty@{E}.
+Print PWrap@{E}.
+
+(* Also works for About. *)
+About punwrap@{K}.
+
+(* Instance length check. *)
+Fail Print foo@{E}.
+Fail Print mono@{E}.
+
+(* Not everything can be printed with custom universe names. *)
+Fail Print Coq.Init.Logic@{E}.
+
+(* Nice error when constraints are impossible. *)
+Monomorphic Universes gU gV. Monomorphic Constraint gU < gV.
+Fail Lemma foo@{u v|u < gU, gV < v, v < u} : nat.
+
+(* Universe binders survive through compilation, sections and modules. *)
+Require TestSuite.bind_univs.
+Print bind_univs.mono.
+Print bind_univs.poly.
+
+Section SomeSec.
+  Universe u.
+  Definition insec@{v} := Type@{u} -> Type@{v}.
+  Print insec.
+End SomeSec.
+Print insec.
+
+Module SomeMod.
+  Definition inmod@{u} := Type@{u}.
+  Print inmod.
+End SomeMod.
+Print SomeMod.inmod.
+Import SomeMod.
+Print inmod.
+
+Module Type SomeTyp. Definition inmod := Type. End SomeTyp.
+Module SomeFunct (In : SomeTyp).
+  Definition infunct@{u v} := In.inmod@{u} -> Type@{v}.
+End SomeFunct.
+Module Applied := SomeFunct(SomeMod).
+Print Applied.infunct.
+
+(* Multi-axiom declaration
+
+   In polymorphic mode the domain Type gets separate universes for the
+   different axioms, but all axioms have to declare all universes. In
+   polymorphic mode they get the same universes, ie the type is only
+   interpd once. *)
+Axiom axfoo@{i+} axbar : Type -> Type@{i}.
+Monomorphic Axiom axfoo'@{i+} axbar' : Type -> Type@{i}.
+
+About axfoo. About axbar. About axfoo'. About axbar'.
+
+Fail Axiom failfoo failbar@{i} : Type.
diff --git a/test-suite/output/ltac.out b/test-suite/output/ltac.out
index 35c3057d8..eb9f57102 100644
--- a/test-suite/output/ltac.out
+++ b/test-suite/output/ltac.out
@@ -1,7 +1,7 @@
 The command has indeed failed with message:
 Ltac variable y depends on pattern variable name z which is not bound in current context.
 Ltac f x y z :=
-  symmetry in x, y; auto with z; auto; intros **; clearbody x; generalize
+  symmetry in x, y; auto with z; auto; intros; clearbody x; generalize
    dependent z
 The command has indeed failed with message:
 In nested Ltac calls to "g1" and "refine (uconstr)", last call failed.
@@ -31,3 +31,10 @@ nat
 nat
 0
 0
+Ltac foo :=
+  let x := intros in
+  let y := intros -> in
+  let v := constr:(nil) in
+  let w := () in
+  let z := 1 in
+  pose v
diff --git a/test-suite/output/ltac.v b/test-suite/output/ltac.v
index 76c37625a..6adbe95dd 100644
--- a/test-suite/output/ltac.v
+++ b/test-suite/output/ltac.v
@@ -57,3 +57,14 @@ match goal with |- ?x*?y => idtac x end.
 match goal with H: context [?x*?y] |- _ => idtac x end.
 match goal with |- context [?x*?y] => idtac x end.
 Abort.
+
+(* Check printing of let in Ltac and Tactic Notation *)
+
+Ltac foo :=
+  let x := intros in
+  let y := intros -> in
+  let v := constr:(@ nil True) in
+  let w := () in
+  let z := 1 in
+  pose v.
+Print Ltac foo.
diff --git a/test-suite/output/ltac_missing_args.out b/test-suite/output/ltac_missing_args.out
index 172612405..7326f137c 100644
--- a/test-suite/output/ltac_missing_args.out
+++ b/test-suite/output/ltac_missing_args.out
@@ -1,20 +1,40 @@
 The command has indeed failed with message:
-A fully applied tactic is expected: missing argument for variable x.
+The user-defined tactic "Top.foo" was not fully applied:
+There is a missing argument for variable x,
+no arguments at all were provided.
 The command has indeed failed with message:
-A fully applied tactic is expected: missing argument for variable x.
+The user-defined tactic "Top.bar" was not fully applied:
+There is a missing argument for variable x,
+no arguments at all were provided.
 The command has indeed failed with message:
-A fully applied tactic is expected: missing arguments for variables y and _.
+The user-defined tactic "Top.bar" was not fully applied:
+There are missing arguments for variables y and _,
+an argument was provided for variable x.
 The command has indeed failed with message:
-A fully applied tactic is expected: missing argument for variable x.
+The user-defined tactic "Top.baz" was not fully applied:
+There is a missing argument for variable x,
+no arguments at all were provided.
 The command has indeed failed with message:
-A fully applied tactic is expected: missing argument for variable x.
+The user-defined tactic "Top.qux" was not fully applied:
+There is a missing argument for variable x,
+no arguments at all were provided.
 The command has indeed failed with message:
-A fully applied tactic is expected: missing argument for variable _.
+The user-defined tactic "Top.mydo" was not fully applied:
+There is a missing argument for variable _,
+no arguments at all were provided.
 The command has indeed failed with message:
-A fully applied tactic is expected: missing argument for variable _.
+An unnamed user-defined tactic was not fully applied:
+There is a missing argument for variable _,
+no arguments at all were provided.
 The command has indeed failed with message:
-A fully applied tactic is expected: missing argument for variable _.
+An unnamed user-defined tactic was not fully applied:
+There is a missing argument for variable _,
+no arguments at all were provided.
 The command has indeed failed with message:
-A fully applied tactic is expected: missing argument for variable x.
+The user-defined tactic "Top.rec" was not fully applied:
+There is a missing argument for variable x,
+no arguments at all were provided.
 The command has indeed failed with message:
-A fully applied tactic is expected: missing argument for variable x.
+An unnamed user-defined tactic was not fully applied:
+There is a missing argument for variable x,
+an argument was provided for variable tac.