12 files changed, 46 insertions, 11 deletions
diff --git a/test-suite/output/Errors.v b/test-suite/output/Errors.v
index edc35f17b4..b52537dec0 100644
--- a/test-suite/output/Errors.v
+++ b/test-suite/output/Errors.v
@@ -1,6 +1,8 @@
 (* coq-prog-args: ("-top" "Errors") *)
 (* Test error messages *)
 
+Set Ltac Backtrace.
+
 (* Test non-regression of bug fixed in r13486 (bad printer for module names) *)
 
 Module Type S.
diff --git a/test-suite/output/FunExt.out b/test-suite/output/FunExt.out
index 8d2a125c1d..2a823396d5 100644
--- a/test-suite/output/FunExt.out
+++ b/test-suite/output/FunExt.out
@@ -1,19 +1,12 @@
 The command has indeed failed with message:
-Ltac call to "extensionality in (var)" failed.
 Tactic failure: Not an extensional equality.
 The command has indeed failed with message:
-Ltac call to "extensionality in (var)" failed.
 Tactic failure: Not an extensional equality.
 The command has indeed failed with message:
-Ltac call to "extensionality in (var)" failed.
 Tactic failure: Not an extensional equality.
 The command has indeed failed with message:
-Ltac call to "extensionality in (var)" failed.
 Tactic failure: Not an extensional equality.
 The command has indeed failed with message:
-Ltac call to "extensionality in (var)" failed.
 Tactic failure: Already an intensional equality.
 The command has indeed failed with message:
-In nested Ltac calls to "extensionality in (var)" and
-"clearbody (ne_var_list)", last call failed.
 Hypothesis e depends on the body of H'
diff --git a/test-suite/output/Notations4.out b/test-suite/output/Notations4.out
index efa895d709..5bf4ec7bfb 100644
--- a/test-suite/output/Notations4.out
+++ b/test-suite/output/Notations4.out
@@ -53,3 +53,23 @@ Notation Cn := Foo.FooCn
 Expands to: Notation Notations4.J.Mfoo.Foo.Bar.Cn
 let v := 0%test17 in v : myint63
      : myint63
+fun y : nat => # (x, z) |-> y & y
+     : forall y : nat,
+       (?T1 * ?T2 -> ?T1 * ?T2 * nat) * (?T * ?T0 -> ?T * ?T0 * nat)
+where
+?T : [y : nat  pat : ?T * ?T0  p0 : ?T * ?T0  p := p0 : ?T * ?T0
+     |- Type] (pat, p0, p cannot be used)
+?T0 : [y : nat  pat : ?T * ?T0  p0 : ?T * ?T0  p := p0 : ?T * ?T0
+      |- Type] (pat, p0, p cannot be used)
+?T1 : [y : nat  pat : ?T1 * ?T2  p0 : ?T1 * ?T2  p := p0 : ?T1 * ?T2
+      |- Type] (pat, p0, p cannot be used)
+?T2 : [y : nat  pat : ?T1 * ?T2  p0 : ?T1 * ?T2  p := p0 : ?T1 * ?T2
+      |- Type] (pat, p0, p cannot be used)
+fun y : nat => # (x, z) |-> (x + y) & (y + z)
+     : forall y : nat,
+       (nat * ?T -> nat * ?T * nat) * (?T0 * nat -> ?T0 * nat * nat)
+where
+?T : [y : nat  pat : nat * ?T  p0 : nat * ?T  p := p0 : nat * ?T
+     |- Type] (pat, p0, p cannot be used)
+?T0 : [y : nat  pat : ?T0 * nat  p0 : ?T0 * nat  p := p0 : ?T0 * nat
+      |- Type] (pat, p0, p cannot be used)
diff --git a/test-suite/output/Notations4.v b/test-suite/output/Notations4.v
index b4c65ce196..b33ad17ed4 100644
--- a/test-suite/output/Notations4.v
+++ b/test-suite/output/Notations4.v
@@ -210,3 +210,12 @@ Module NumeralNotations.
     Check let v := 0%test17 in v : myint63.
   End Test17.
 End NumeralNotations.
+
+Module K.
+
+Notation "# x |-> t & u" := ((fun x => (x,t)),(fun x => (x,u)))
+  (at level 0, x pattern, t, u at level 39).
+Check fun y : nat => # (x,z) |-> y & y.
+Check fun y : nat => # (x,z) |-> (x + y) & (y + z).
+
+End K.
diff --git a/test-suite/output/TypeclassDebug.out b/test-suite/output/TypeclassDebug.out
index 8b38fe0ff4..7ea7a08cb3 100644
--- a/test-suite/output/TypeclassDebug.out
+++ b/test-suite/output/TypeclassDebug.out
@@ -14,5 +14,4 @@ Debug: 1.1-1.1-1.1-1.1-1: looking for foo without backtracking
 Debug: 1.1-1.1-1.1-1.1-1.1: simple apply H on foo, 1 subgoal(s)
 Debug: 1.1-1.1-1.1-1.1-1.1-1 : foo
 The command has indeed failed with message:
-Ltac call to "typeclasses eauto (int_or_var_opt) with (ne_preident_list)" failed.
 Tactic failure: Proof search reached its limit.
diff --git a/test-suite/output/UnivBinders.out b/test-suite/output/UnivBinders.out
index a960fe3441..222a808768 100644
--- a/test-suite/output/UnivBinders.out
+++ b/test-suite/output/UnivBinders.out
@@ -1,5 +1,7 @@
 Inductive Empty@{u} : Type@{u} :=  
+(* u |=  *)
 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]
@@ -11,6 +13,7 @@ fun (A : Type@{u}) (p : PWrap@{u} A) => punwrap _ p
 
 Argument scopes are [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 _]
@@ -79,7 +82,9 @@ Type@{UnivBinders.17} -> Type@{v} -> Type@{u}
      : Type@{max(u+1,UnivBinders.17+1,v+1)}
 (* u UnivBinders.17 v |=  *)
 Inductive Empty@{E} : Type@{E} :=  
+(* E |=  *)
 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]
@@ -109,7 +114,9 @@ bind_univs.poly@{u} = Type@{u}
 insec@{v} = Type@{u} -> Type@{v}
      : Type@{max(u+1,v+1)}
 (* v |=  *)
-Inductive insecind@{k} : Type@{k+1} :=  inseccstr : Type@{k} -> insecind@{k}
+Inductive insecind@{k} : Type@{k+1} :=
+    inseccstr : Type@{k} -> insecind@{k}
+(* k |=  *)
 
 For inseccstr: Argument scope is [type_scope]
 insec@{u v} = Type@{u} -> Type@{v}
@@ -117,6 +124,7 @@ insec@{u v} = Type@{u} -> Type@{v}
 (* u v |=  *)
 Inductive insecind@{u k} : Type@{k+1} :=
     inseccstr : Type@{k} -> insecind@{u k}
+(* u k |=  *)
 
 For inseccstr: Argument scope is [type_scope]
 insec2@{u} = Prop
diff --git a/test-suite/output/bug5778.v b/test-suite/output/bug5778.v
index 0dcd76aeff..441e87af84 100644
--- a/test-suite/output/bug5778.v
+++ b/test-suite/output/bug5778.v
@@ -1,3 +1,4 @@
+Set Ltac Backtrace.
 Ltac a _ := pose (I : I).
 Ltac b _ := a ().
 Ltac abs _ := abstract b ().
diff --git a/test-suite/output/bug6404.v b/test-suite/output/bug6404.v
index bbe6b1a00f..d9e5e20b66 100644
--- a/test-suite/output/bug6404.v
+++ b/test-suite/output/bug6404.v
@@ -1,3 +1,4 @@
+Set Ltac Backtrace.
 Ltac a _ := pose (I : I).
 Ltac b _ := a ().
 Ltac abs _ := transparent_abstract b ().
diff --git a/test-suite/output/ltac.v b/test-suite/output/ltac.v
index 40e743c3f0..fcd5dd05f0 100644
--- a/test-suite/output/ltac.v
+++ b/test-suite/output/ltac.v
@@ -1,3 +1,5 @@
+Set Ltac Backtrace.
+
 (* This used to refer to b instead of z sometimes between 8.4 and 8.5beta3 *)
 Goal True.
 Fail let T := constr:((fun a b : nat => a+b) 1 1) in
diff --git a/test-suite/output/ltac_missing_args.v b/test-suite/output/ltac_missing_args.v
index 91331a1de5..e30c97aac6 100644
--- a/test-suite/output/ltac_missing_args.v
+++ b/test-suite/output/ltac_missing_args.v
@@ -1,3 +1,5 @@
+Set Ltac Backtrace.
+
 Ltac foo x := idtac x.
 Ltac bar x := fun y _ => idtac x y.
 Ltac baz := foo.
diff --git a/test-suite/output/ssr_clear.out b/test-suite/output/ssr_clear.out
index 1515954060..1a0f90493e 100644
--- a/test-suite/output/ssr_clear.out
+++ b/test-suite/output/ssr_clear.out
@@ -1,3 +1,2 @@
 The command has indeed failed with message:
-Ltac call to "move (ssrmovearg) (ssrclauses)" failed.
 No assumption is named NO_SUCH_NAME
diff --git a/test-suite/output/ssr_explain_match.out b/test-suite/output/ssr_explain_match.out
index 32cfb354bf..0f68ab0b02 100644
--- a/test-suite/output/ssr_explain_match.out
+++ b/test-suite/output/ssr_explain_match.out
@@ -51,5 +51,4 @@ instance: (addnC y x) matches: (x + y)
 instance: (addnC y x) matches: (x + y)
 END INSTANCES
 The command has indeed failed with message:
-Ltac call to "ssrinstancesoftpat (cpattern)" failed.
 Not supported