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

8 files changed, 36 insertions, 21 deletions

diff --git a/library/impargs.ml b/library/impargs.ml
index 4cf8e98228..badb69cb1e 100644
--- a/library/impargs.ml
+++ b/library/impargs.ml
@@ -466,7 +466,8 @@ let implicits_of_global ref =
        | _ -> imp in
       List.map2 (fun (t, il) rl -> t, List.map2 rename il rl) l rename_l
     with Not_found -> l
-    | Invalid_argument _ -> anomaly "renaming implicits"
+    | Invalid_argument _ ->
+        anomaly "renamings list and implicits list have different lenghts"
   with Not_found -> [DefaultImpArgs,[]]
 
 let cache_implicits_decl (ref,imps) =
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index 2dc72f658f..756f1d5186 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -659,6 +659,7 @@ GEXTEND Gram
       | IDENT "default"; IDENT "implicits" -> [`DefaultImplicits]
       | IDENT "clear"; IDENT "implicits" -> [`ClearImplicits]
       | IDENT "clear"; IDENT "scopes" -> [`ClearScopes]
+      | IDENT "rename" -> [`Rename]
       | IDENT "clear"; IDENT "scopes"; IDENT "and"; IDENT "implicits" ->
           [`ClearImplicits; `ClearScopes]
       | IDENT "clear"; IDENT "implicits"; IDENT "and"; IDENT "scopes" ->
diff --git a/parsing/ppvernac.ml b/parsing/ppvernac.ml
index 4e73b37939..27de53cada 100644
--- a/parsing/ppvernac.ml
+++ b/parsing/ppvernac.ml
@@ -857,6 +857,7 @@ let rec pr_vernac = function
         | `SimplDontExposeCase -> str "simpl nomatch"
         | `SimplNeverUnfold -> str "simpl never"
         | `DefaultImplicits -> str "default implicits"
+        | `Rename -> str "rename"
         | `ClearImplicits -> str "clear implicits"
         | `ClearScopes -> str "clear scopes")
         mods)
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.
+
+
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index a38f7ce36d..110e6190c5 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -780,30 +780,35 @@ let vernac_declare_arguments local r l nargs flags =
     | l, [] -> error ("The following arguments are not declared: " ^
        (String.concat ", " (List.map string_of_name l)))
     | _::li, _::ld -> check li ld in
-  if names <> [] then
+  if l <> [[]] then
     List.iter (fun l -> check inf_names l) (names :: rest);
+  (* we interpret _ as the inferred names *)
+  let l = if l = [[]] then l else
+    let name_anons = function
+      | (Anonymous, a,b,c,d), Name id -> Name id, a,b,c,d
+      | x, _ -> x in
+    List.map (fun ns -> List.map name_anons (List.combine ns inf_names)) l in
+  let names_decl = List.map (List.map (fun (id, _,_,_,_) -> id)) l in
+  let some_renaming_specified =
+    try Arguments_renaming.arguments_names sr <> names_decl
+    with Not_found -> false in
   let some_renaming_specified, implicits =
-    if names = [] then false, [[]] else
-    let never_implicit x =
-      not (List.exists (List.exists (fun (y, _,_, b, _) -> b && y = x)) l) in
+    if l = [[]] then false, [[]] else
     Util.list_fold_map (fun sr il ->
       let sr', impl = Util.list_fold_map (fun b -> function
-        | (Anonymous, _,_, true, _), _ ->
-            error "Implicit arguments must have a name"
-        | (Name x,_,_,false,_),Name y when x <> y && never_implicit (Name x)->
-            error ("Reanaming a non implicit argument " ^ string_of_id y ^
-              " to " ^ string_of_id x)
+        | (Anonymous, _,_, true, max), Name id -> assert false
         | (Name x, _,_, true, _), Anonymous ->
-            error ("Argument "^string_of_id x^" is anonymous and cannot be"^
-              " declared implicit")
+            error ("Argument "^string_of_id x^" cannot be declared implicit")
         | (Name iid, _,_, true, max), Name id ->
            b || iid <> id, Some (ExplByName id, max, false)
         | _ -> b, None)
-        false (List.combine il inf_names) in
+        sr (List.combine il inf_names) in
       sr || sr', Util.list_map_filter (fun x -> x) impl)
-      false l in
+      some_renaming_specified l in
   if some_renaming_specified then
-    Arguments_renaming.rename_arguments local sr (names :: rest);
+    if not (List.mem `Rename flags) then
+      error "to rename arguments the \"rename\" flag must be specified"
+    else Arguments_renaming.rename_arguments local sr names_decl;
   (* All other infos are in the first item of l *)
   let l = List.hd l in
   let some_implicits_specified = implicits <> [[]] in
diff --git a/toplevel/vernacexpr.ml b/toplevel/vernacexpr.ml
index 575735230d..33a474923f 100644
--- a/toplevel/vernacexpr.ml
+++ b/toplevel/vernacexpr.ml
@@ -318,7 +318,7 @@ type vernac_expr =
       (explicitation * bool * bool) list list
   | VernacArguments of locality_flag * reference or_by_notation * 
       ((name * bool * (loc * string) option * bool * bool) list) list *
-      int * [ `SimplDontExposeCase | `SimplNeverUnfold
+      int * [ `SimplDontExposeCase | `SimplNeverUnfold | `Rename
             | `ClearImplicits | `ClearScopes | `DefaultImplicits ] list
   | VernacArgumentsScope of locality_flag * reference or_by_notation *
       scope_name option list