11 files changed, 77 insertions, 4 deletions
diff --git a/test-suite/output/Fixpoint.v b/test-suite/output/Fixpoint.v
index fafb478bad..61ae4edbd1 100644
--- a/test-suite/output/Fixpoint.v
+++ b/test-suite/output/Fixpoint.v
@@ -7,7 +7,7 @@ Check
              | a :: l => f a :: F _ _ f l
              end).
 
-(* V8 printing of this term used to failed in V8.0 and V8.0pl1 (cf bug #860) *)
+(* V8 printing of this term used to failed in V8.0 and V8.0pl1 (cf BZ#860) *)
 Check
   let fix f (m : nat) : nat :=
     match m with
diff --git a/test-suite/output/Implicit.v b/test-suite/output/Implicit.v
index 7c9b89f9d2..306532c0df 100644
--- a/test-suite/output/Implicit.v
+++ b/test-suite/output/Implicit.v
@@ -1,7 +1,7 @@
 Set Implicit Arguments.
 Unset Strict Implicit.
 
-(* Suggested by Pierre Casteran (bug #169) *)
+(* Suggested by Pierre Casteran (BZ#169) *)
 (* Argument 3 is needed to typecheck and should be printed *)
 Definition compose (A B C : Set) (f : A -> B) (g : B -> C) (x : A) := g (f x).
 Check (compose (C:=nat) S).
diff --git a/test-suite/output/Notations3.out b/test-suite/output/Notations3.out
index 65efe228af..6ef75dd135 100644
--- a/test-suite/output/Notations3.out
+++ b/test-suite/output/Notations3.out
@@ -124,3 +124,7 @@ return (1, 2, 3, 4)
      : nat
 !!! _ _ : nat, True
      : (nat -> Prop) * ((nat -> Prop) * Prop)
+((*1).2).3
+     : nat
+*(1.2)
+     : nat
diff --git a/test-suite/output/Notations3.v b/test-suite/output/Notations3.v
index ea372ad1a3..8c7bbe5917 100644
--- a/test-suite/output/Notations3.v
+++ b/test-suite/output/Notations3.v
@@ -190,3 +190,10 @@ Check 1+1+1.
 (* 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).
 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").
+Check (((id 1) + 2) + 3).
+Check (id (1 + 2)).
diff --git a/test-suite/output/SuggestProofUsing.out b/test-suite/output/SuggestProofUsing.out
new file mode 100644
index 0000000000..8d67a4a4b7
--- /dev/null
+++ b/test-suite/output/SuggestProofUsing.out
@@ -0,0 +1,7 @@
+The proof of nat should start with one of the following commands:
+Proof using . 
+Proof using Type*. 
+Proof using Type. 
+The proof of foo should start with one of the following commands:
+Proof using A B. 
+Proof using All. 
diff --git a/test-suite/output/SuggestProofUsing.v b/test-suite/output/SuggestProofUsing.v
new file mode 100644
index 0000000000..00b6f8e183
--- /dev/null
+++ b/test-suite/output/SuggestProofUsing.v
@@ -0,0 +1,31 @@
+Set Suggest Proof Using.
+
+Section Sec.
+  Variables A B : Type.
+
+  (* Some normal lemma. *)
+  Lemma nat : Set.
+  Proof.
+    exact nat.
+  Qed.
+
+  (* Make sure All is suggested even though we add an unused variable
+  to the context. *)
+  Let foo : Type.
+  Proof.
+    exact (A -> B).
+  Qed.
+
+  (* Having a [Proof using] disables the suggestion message. *)
+  Definition bar : Type.
+  Proof using A.
+    exact A.
+  Qed.
+
+  (* Transparent definitions don't get a suggestion message. *)
+  Definition baz : Type.
+  Proof.
+    exact A.
+  Defined.
+
+End Sec.
diff --git a/test-suite/output/Tactics.v b/test-suite/output/Tactics.v
index 9a5edb813d..75b66e463a 100644
--- a/test-suite/output/Tactics.v
+++ b/test-suite/output/Tactics.v
@@ -7,12 +7,12 @@ Ltac f H := split; [a H|e H].
 Print Ltac f.
 
 (* Test printing of match context *)
-(* Used to fail after translator removal (see bug #1070) *)
+(* Used to fail after translator removal (see BZ#1070) *)
 
 Ltac g := match goal with |- context [if ?X then _ else _ ] => case X end.
 Print Ltac g.
 
-(* Test an error message (#5390) *)
+(* Test an error message (BZ#5390) *)
 Lemma myid (P : Prop) : P <-> P.
 Proof. split; auto. Qed.
 
diff --git a/test-suite/output/auto.out b/test-suite/output/auto.out
index a5b55a9993..2761b87b02 100644
--- a/test-suite/output/auto.out
+++ b/test-suite/output/auto.out
@@ -18,3 +18,5 @@ Debug: 1 depth=5
 Debug: 1.1 depth=4 simple apply or_intror
 Debug: 1.1.1 depth=4 intro
 Debug: 1.1.1.1 depth=4 exact H
+(* info trivial: *)
+exact I (in core).
diff --git a/test-suite/output/auto.v b/test-suite/output/auto.v
index a77b7b82e6..92917cdfc7 100644
--- a/test-suite/output/auto.v
+++ b/test-suite/output/auto.v
@@ -9,3 +9,7 @@ info_eauto.
 Undo.
 debug eauto.
 Qed.
+
+Goal True.
+info_trivial.
+Qed.
diff --git a/test-suite/output/ltac_extra_args.out b/test-suite/output/ltac_extra_args.out
new file mode 100644
index 0000000000..77e799d359
--- /dev/null
+++ b/test-suite/output/ltac_extra_args.out
@@ -0,0 +1,8 @@
+The command has indeed failed with message:
+Illegal tactic application: got 1 extra argument.
+The command has indeed failed with message:
+Illegal tactic application: got 2 extra arguments.
+The command has indeed failed with message:
+Illegal tactic application: got 1 extra argument.
+The command has indeed failed with message:
+Illegal tactic application: got 2 extra arguments.
diff --git a/test-suite/output/ltac_extra_args.v b/test-suite/output/ltac_extra_args.v
new file mode 100644
index 0000000000..4caf619fee
--- /dev/null
+++ b/test-suite/output/ltac_extra_args.v
@@ -0,0 +1,10 @@
+Ltac foo := idtac.
+Ltac bar H := idtac.
+
+Goal True.
+Proof.
+  Fail foo H.
+  Fail foo H H'.
+  Fail bar H H'.
+  Fail bar H H' H''.
+Abort.