Minor fixes to Arguments

- Implicit arguments can be mentioned anonymously:

    Arguments map {_ _} f l.

- To rename implicit arguments, the ": rename" flag must be used:

    Arguments map {T1 T2} f l : rename.

  Without the ": rename" flag arguments can be used to assert
  that a function has indeed the expected number of arguments and
  that the arguments are named as expected.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14766 85f007b7-540e-0410-9357-904b9bb8a0f7

3 files changed, 12 insertions, 5 deletions

diff --git a/test-suite/output/Arguments.v b/test-suite/output/Arguments.v
index c93d2505da..3a94f19a71 100644
--- a/test-suite/output/Arguments.v
+++ b/test-suite/output/Arguments.v
@@ -14,7 +14,7 @@ Delimit Scope foo_scope with F.
 Arguments pf {D1%F C1%type} f [D2 C2] g x : simpl never.
 About pf.
 Definition fcomp A B C f (g : A -> B) (x : A) : C := f (g x).
-Arguments fcomp {A B C}%type_scope f g x /.
+Arguments fcomp {_ _ _}%type_scope f g x /.
 About fcomp.
 Definition volatile := fun x : nat => x.
 Arguments volatile /.
diff --git a/test-suite/output/Arguments_renaming.out b/test-suite/output/Arguments_renaming.out
index ed08334e73..925ff693a7 100644
--- a/test-suite/output/Arguments_renaming.out
+++ b/test-suite/output/Arguments_renaming.out
@@ -1,3 +1,5 @@
+The command has indeed failed with message:
+=> Error: to rename arguments the "rename" flag must be specified
 @eq_refl
      : forall (B : Type) (y : B), y = y
 eq_refl
@@ -99,6 +101,6 @@ The command has indeed failed with message:
 The command has indeed failed with message:
 => Error: Arguments names must be distinct
 The command has indeed failed with message:
-=> Error: Argument z is anonymous and cannot be declared implicit
+=> Error: Argument z cannot be declared implicit
 The command has indeed failed with message:
 => Error: Extra argument y
diff --git a/test-suite/output/Arguments_renaming.v b/test-suite/output/Arguments_renaming.v
index 7cbb6801ea..e9b5f247ec 100644
--- a/test-suite/output/Arguments_renaming.v
+++ b/test-suite/output/Arguments_renaming.v
@@ -1,4 +1,7 @@
-Arguments eq_refl {B y}, [B] y.
+Fail Arguments eq_refl {B y}, [B] y.
+Arguments eq_refl A x.
+Arguments eq_refl {B y}, [B] y : rename.
+
 Check @eq_refl.
 Check (eq_refl (B := nat)).
 Print eq_refl.
@@ -19,14 +22,14 @@ Variable A : Type.
 
 Inductive myEq B (x : A) : A -> Prop := myrefl : B -> myEq B x x.
 
-Global Arguments myrefl {C} x _.
+Global Arguments myrefl {C} x _ : rename.
 Print myrefl.
 About myrefl.
 
 Fixpoint myplus T (t : T) (n m : nat) {struct n} :=
   match n with O => m | S n' => S (myplus T t n' m) end.
 
-Global Arguments myplus {Z} !t !n m.
+Global Arguments myplus {Z} !t !n m : rename.
 
 Print myplus.
 About myplus.
@@ -46,3 +49,5 @@ Fail Arguments eq_refl {F}, [F].
 Fail Arguments eq_refl {F F}, [F] F.
 Fail Arguments eq {F} x [z].
 Fail Arguments eq {F} x z y.
+
+