6 files changed, 35 insertions, 0 deletions
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/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.