Merge branch 'trunk' into pr379

8 files changed, 62 insertions, 24 deletions

diff --git a/test-suite/output/Arguments.out b/test-suite/output/Arguments.out
index a2ee2d4c8e..979396969a 100644
--- a/test-suite/output/Arguments.out
+++ b/test-suite/output/Arguments.out
@@ -97,8 +97,8 @@ Expands to: Constant Top.f
 forall w : r, w 3 true = tt
      : Prop
 The command has indeed failed with message:
-Error: Unknown interpretation for notation "$".
+Unknown interpretation for notation "$".
 w 3 true = tt
      : Prop
 The command has indeed failed with message:
-Error: Extra arguments: _, _.
+Extra arguments: _, _.
diff --git a/test-suite/output/Arguments_renaming.out b/test-suite/output/Arguments_renaming.out
index b084ad4984..4df21ae353 100644
--- a/test-suite/output/Arguments_renaming.out
+++ b/test-suite/output/Arguments_renaming.out
@@ -1,5 +1,5 @@
 The command has indeed failed with message:
-Error: To rename arguments the "rename" flag must be specified.
+To rename arguments the "rename" flag must be specified.
 Argument A renamed to B.
 File "stdin", line 2, characters 0-25:
 Warning: This command is just asserting the names of arguments of identity.
@@ -103,15 +103,15 @@ Expands to: Constant Top.myplus
 @myplus
      : forall Z : Type, Z -> nat -> nat -> nat
 The command has indeed failed with message:
-Error: Argument lists should agree on the names they provide.
+Argument lists should agree on the names they provide.
 The command has indeed failed with message:
-Error: Sequences of implicit arguments must be of different lengths.
+Sequences of implicit arguments must be of different lengths.
 The command has indeed failed with message:
-Error: Some argument names are duplicated: F
+Some argument names are duplicated: F
 The command has indeed failed with message:
-Error: Argument z cannot be declared implicit.
+Argument z cannot be declared implicit.
 The command has indeed failed with message:
-Error: Extra arguments: y.
+Extra arguments: y.
 The command has indeed failed with message:
-Error: To rename arguments the "rename" flag must be specified.
+To rename arguments the "rename" flag must be specified.
 Argument A renamed to R.
diff --git a/test-suite/output/Errors.out b/test-suite/output/Errors.out
index 06a6b2d157..38d055b28e 100644
--- a/test-suite/output/Errors.out
+++ b/test-suite/output/Errors.out
@@ -7,4 +7,4 @@ In nested Ltac calls to "f" and "apply x", last call failed.
 Unable to unify "nat" with "True".
 The command has indeed failed with message:
 Ltac call to "instantiate ( (ident) := (lglob) )" failed.
-Error: Instance is not well-typed in the environment of ?x.
+Instance is not well-typed in the environment of ?x.
diff --git a/test-suite/output/FunExt.out b/test-suite/output/FunExt.out
index c6786c72ff..8d2a125c1d 100644
--- a/test-suite/output/FunExt.out
+++ b/test-suite/output/FunExt.out
@@ -16,4 +16,4 @@ 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.
-Error: Hypothesis e depends on the body of H'
+Hypothesis e depends on the body of H'
diff --git a/test-suite/output/Notations.out b/test-suite/output/Notations.out
index 26eaca8272..9d106d2dac 100644
--- a/test-suite/output/Notations.out
+++ b/test-suite/output/Notations.out
@@ -41,29 +41,29 @@ fun x : nat => ifn x is succ n then n else 0
 -4
      : Z
 The command has indeed failed with message:
-Error: x should not be bound in a recursive pattern of the right-hand side.
+x should not be bound in a recursive pattern of the right-hand side.
 The command has indeed failed with message:
-Error: in the right-hand side, y and z should appear in
+in the right-hand side, y and z should appear in
 term position as part of a recursive pattern.
 The command has indeed failed with message:
 The reference w was not found in the current environment.
 The command has indeed failed with message:
-Error: in the right-hand side, y and z should appear in
+in the right-hand side, y and z should appear in
 term position as part of a recursive pattern.
 The command has indeed failed with message:
-Error: z is expected to occur in binding position in the right-hand side.
+z is expected to occur in binding position in the right-hand side.
 The command has indeed failed with message:
-Error: as y is a non-closed binder, no such "," is allowed to occur.
+as y is a non-closed binder, no such "," is allowed to occur.
 The command has indeed failed with message:
-Error: Cannot find where the recursive pattern starts.
+Cannot find where the recursive pattern starts.
 The command has indeed failed with message:
-Error: Cannot find where the recursive pattern starts.
+Cannot find where the recursive pattern starts.
 The command has indeed failed with message:
-Error: Cannot find where the recursive pattern starts.
+Cannot find where the recursive pattern starts.
 The command has indeed failed with message:
-Error: Cannot find where the recursive pattern starts.
+Cannot find where the recursive pattern starts.
 The command has indeed failed with message:
-Error: Both ends of the recursive pattern are the same.
+Both ends of the recursive pattern are the same.
 SUM (nat * nat) nat
      : Set
 FST (0; 1)
diff --git a/test-suite/output/ltac.out b/test-suite/output/ltac.out
index 1ff09e3af6..35c3057d84 100644
--- a/test-suite/output/ltac.out
+++ b/test-suite/output/ltac.out
@@ -1,5 +1,4 @@
 The command has indeed failed with message:
-Error:
 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
@@ -22,11 +21,11 @@ The term "I" has type "True" while it is expected to have type "False".
 The command has indeed failed with message:
 In nested Ltac calls to "h" and "injection (destruction_arg)", last call
 failed.
-Error: No primitive equality found.
+No primitive equality found.
 The command has indeed failed with message:
 In nested Ltac calls to "h" and "injection (destruction_arg)", last call
 failed.
-Error: No primitive equality found.
+No primitive equality found.
 Hx
 nat
 nat
diff --git a/test-suite/output/ltac_missing_args.out b/test-suite/output/ltac_missing_args.out
new file mode 100644
index 0000000000..172612405f
--- /dev/null
+++ b/test-suite/output/ltac_missing_args.out
@@ -0,0 +1,20 @@
+The command has indeed failed with message:
+A fully applied tactic is expected: missing argument for variable x.
+The command has indeed failed with message:
+A fully applied tactic is expected: missing argument for variable x.
+The command has indeed failed with message:
+A fully applied tactic is expected: missing arguments for variables y and _.
+The command has indeed failed with message:
+A fully applied tactic is expected: missing argument for variable x.
+The command has indeed failed with message:
+A fully applied tactic is expected: missing argument for variable x.
+The command has indeed failed with message:
+A fully applied tactic is expected: missing argument for variable _.
+The command has indeed failed with message:
+A fully applied tactic is expected: missing argument for variable _.
+The command has indeed failed with message:
+A fully applied tactic is expected: missing argument for variable _.
+The command has indeed failed with message:
+A fully applied tactic is expected: missing argument for variable x.
+The command has indeed failed with message:
+A fully applied tactic is expected: missing argument for variable x.
diff --git a/test-suite/output/ltac_missing_args.v b/test-suite/output/ltac_missing_args.v
new file mode 100644
index 0000000000..8ecd97aa56
--- /dev/null
+++ b/test-suite/output/ltac_missing_args.v
@@ -0,0 +1,19 @@
+Ltac foo x := idtac x.
+Ltac bar x := fun y _ => idtac x y.
+Ltac baz := foo.
+Ltac qux := bar.
+Ltac mydo tac := tac ().
+Ltac rec x := rec.
+
+Goal True.
+  Fail foo.
+  Fail bar.
+  Fail bar True.
+  Fail baz.
+  Fail qux.
+  Fail mydo ltac:(fun _ _ => idtac).
+  Fail let tac := (fun _ => idtac) in tac.
+  Fail (fun _ => idtac).
+  Fail rec True.
+  Fail let rec tac x := tac in tac True.
+Abort.
\ No newline at end of file