Complete overhaul of the Arguments vernacular.

The main point of this change is to fix #3035: Avoiding trailing
arguments in the Arguments command, and related issues occurring in
HoTT for instance. When the "assert" flag is not specified, we now
accept prefixes of the list of arguments.

The semantics of _ w.r.t. to renaming has changed. Previously, it meant
"restore the original name inferred from the type". Now it means "don't
change the current name".

The syntax of arguments is now restricted. Modifiers like /, ! and
scopes are allowed only in the first arguments list.

We also add *a lot* of missing checks on input values and fix various
bugs.

Note that this code is still way too complex for what it does, due to
the complexity of the implicit arguments, reduction behaviors and renaming
APIs.

12 files changed, 344 insertions, 254 deletions

diff --git a/intf/vernacexpr.mli b/intf/vernacexpr.mli
index 857287040..1336c92b6 100644
--- a/intf/vernacexpr.mli
+++ b/intf/vernacexpr.mli
@@ -416,10 +416,12 @@ type vernac_expr =
   | VernacDeclareImplicits of reference or_by_notation *
       (explicitation * bool * bool) list list
   | VernacArguments of reference or_by_notation *
-      (vernac_argument_status list) list *
-      int * [ `ReductionDontExposeCase | `ReductionNeverUnfold | `Rename |
-              `ExtraScopes | `Assert | `ClearImplicits | `ClearScopes |
-              `DefaultImplicits ] list
+      vernac_argument_status list (* Main arguments status list *) *
+        (Name.t * vernac_implicit_status) list list (* Extra implicit status lists *) *
+      int option (* Number of args to trigger reduction *) *
+        [ `ReductionDontExposeCase | `ReductionNeverUnfold | `Rename |
+          `ExtraScopes | `Assert | `ClearImplicits | `ClearScopes |
+          `DefaultImplicits ] list
   | VernacArgumentsScope of reference or_by_notation *
       scope_name option list
   | VernacReserve of simple_binder list
@@ -479,11 +481,13 @@ and tacdef_body =
   | TacticDefinition of Id.t Loc.located * raw_tactic_expr  (* indicates that user employed ':=' in Ltac body *)
   | TacticRedefinition of reference * raw_tactic_expr       (* indicates that user employed '::=' in Ltac body *)
 
+and vernac_implicit_status = Implicit | MaximallyImplicit | NotImplicit
+
 and vernac_argument_status = {
   name : Name.t;
   recarg_like : bool;
   notation_scope : (Loc.t * string) option;
-  implicit_status : [ `Implicit | `MaximallyImplicit | `NotImplicit];
+  implicit_status : vernac_implicit_status;
 }
 
 (* A vernac classifier has to tell if a command:
diff --git a/library/impargs.ml b/library/impargs.ml
index bce7a15cb..a709aedee 100644
--- a/library/impargs.ml
+++ b/library/impargs.ml
@@ -494,7 +494,7 @@ let implicits_of_global ref =
       let rename imp name = match imp, name with
        | Some (_, x,y), Name id -> Some (id, x,y)
        | _ -> imp in
-      List.map2 (fun (t, il) rl -> t, List.map2 rename il rl) l rename_l
+      List.map (fun (t, il) -> t, List.map2 rename il rename_l) l
     with Not_found -> l
     | Invalid_argument _ ->
         anomaly (Pp.str "renamings list and implicits list have different lenghts")
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index bc02a4621..e0d836df8 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -651,58 +651,29 @@ GEXTEND Gram
 
       (* Arguments *)
       | IDENT "Arguments"; qid = smart_global; 
-        impl = LIST1 [ l = LIST0
-        [ item = argument_spec ->
-            let name, recarg_like, notation_scope = item in
-            [`Id { name=name; recarg_like=recarg_like;
-                   notation_scope=notation_scope;
-                   implicit_status = `NotImplicit}]
-        | "/" -> [`Slash]
-        | "("; items = LIST1 argument_spec; ")"; sc = OPT scope ->
-            let f x = match sc, x with
-            | None, x -> x | x, None -> Option.map (fun y -> !@loc, y) x
-            | Some _, Some _ -> error "scope declared twice" in
-            List.map (fun (name,recarg_like,notation_scope) ->
-              `Id { name=name; recarg_like=recarg_like;
-                    notation_scope=f notation_scope;
-                    implicit_status = `NotImplicit}) items
-        | "["; items = LIST1 argument_spec; "]"; sc = OPT scope ->
-            let f x = match sc, x with
-            | None, x -> x | x, None -> Option.map (fun y -> !@loc, y) x
-            | Some _, Some _ -> error "scope declared twice" in
-            List.map (fun (name,recarg_like,notation_scope) ->
-              `Id { name=name; recarg_like=recarg_like;
-                    notation_scope=f notation_scope;
-                    implicit_status = `Implicit}) items
-        | "{"; items = LIST1 argument_spec; "}"; sc = OPT scope ->
-            let f x = match sc, x with
-            | None, x -> x | x, None -> Option.map (fun y -> !@loc, y) x
-            | Some _, Some _ -> error "scope declared twice" in
-            List.map (fun (name,recarg_like,notation_scope) ->
-              `Id { name=name; recarg_like=recarg_like;
-                    notation_scope=f notation_scope;
-                    implicit_status = `MaximallyImplicit}) items
-        ] -> l ] SEP ",";
+        args = LIST0 argument_spec_block;
+        more_implicits = OPT
+          [ ","; impl = LIST1
+            [ impl = LIST0 more_implicits_block -> List.flatten impl]
+            SEP "," -> impl
+          ];
         mods = OPT [ ":"; l = LIST1 arguments_modifier SEP "," -> l ] ->
          let mods = match mods with None -> [] | Some l -> List.flatten l in
-         let impl = List.map List.flatten impl in
-         let rec aux n (narg, impl) = function
-           | `Id x :: tl -> aux (n+1) (narg, impl@[x]) tl
-           | `Slash :: tl -> aux (n+1) (n, impl) tl
-           | [] -> narg, impl in
-         let nargs, impl = List.split (List.map (aux 0 (-1, [])) impl) in
-         let nargs, rest = List.hd nargs, List.tl nargs in
-         if List.exists (fun arg -> not (Int.equal arg nargs)) rest then
-           error "All arguments lists must have the same length";
-         let err_incompat x y =
-           error ("Options \""^x^"\" and \""^y^"\" are incompatible") in
-         if nargs > 0 && List.mem `ReductionNeverUnfold mods then
-           err_incompat "simpl never" "/";
-         if List.mem `ReductionNeverUnfold mods &&
-            List.mem `ReductionDontExposeCase mods then
-           err_incompat "simpl never" "simpl nomatch";
-         VernacArguments (qid, impl, nargs, mods)
-
+         let slash_position = ref None in
+         let rec parse_args i = function
+           | [] -> []
+           | `Id x :: args -> x :: parse_args (i+1) args
+           | `Slash :: args ->
+              if Option.is_empty !slash_position then
+                (slash_position := Some i; parse_args i args)
+              else
+                error "The \"/\" modifier can occur only once"
+         in
+         let args = parse_args 0 (List.flatten args) in
+         let more_implicits = Option.default [] more_implicits in
+         VernacArguments (qid, args, more_implicits, !slash_position, mods)
+
+ 
      (* moved there so that camlp5 factors it with the previous rule *)
      | IDENT "Arguments"; IDENT "Scope"; qid = smart_global;
        "["; scl = LIST0 [ "_" -> None | sc = IDENT -> Some sc ]; "]" ->
@@ -759,6 +730,49 @@ GEXTEND Gram
        snd id, not (Option.is_empty b), Option.map (fun x -> !@loc, x) s
     ]
   ];
+  (* List of arguments implicit status, scope, modifiers *)
+  argument_spec_block: [
+    [ item = argument_spec ->
+      let name, recarg_like, notation_scope = item in
+      [`Id { name=name; recarg_like=recarg_like;
+             notation_scope=notation_scope;
+             implicit_status = NotImplicit}]
+    | "/" -> [`Slash]
+    | "("; items = LIST1 argument_spec; ")"; sc = OPT scope ->
+       let f x = match sc, x with
+         | None, x -> x | x, None -> Option.map (fun y -> !@loc, y) x
+         | Some _, Some _ -> error "scope declared twice" in
+       List.map (fun (name,recarg_like,notation_scope) ->
+           `Id { name=name; recarg_like=recarg_like;
+                 notation_scope=f notation_scope;
+                 implicit_status = NotImplicit}) items
+    | "["; items = LIST1 argument_spec; "]"; sc = OPT scope ->
+       let f x = match sc, x with
+         | None, x -> x | x, None -> Option.map (fun y -> !@loc, y) x
+         | Some _, Some _ -> error "scope declared twice" in
+       List.map (fun (name,recarg_like,notation_scope) ->
+           `Id { name=name; recarg_like=recarg_like;
+                 notation_scope=f notation_scope;
+                 implicit_status = Implicit}) items
+    | "{"; items = LIST1 argument_spec; "}"; sc = OPT scope ->
+       let f x = match sc, x with
+         | None, x -> x | x, None -> Option.map (fun y -> !@loc, y) x
+         | Some _, Some _ -> error "scope declared twice" in
+       List.map (fun (name,recarg_like,notation_scope) ->
+           `Id { name=name; recarg_like=recarg_like;
+                 notation_scope=f notation_scope;
+                 implicit_status = MaximallyImplicit}) items
+    ]
+  ];
+  (* Same as [argument_spec_block], but with only implicit status and names *)
+  more_implicits_block: [
+    [ name = name -> [(snd name, Vernacexpr.NotImplicit)]
+    | "["; items = LIST1 name; "]" ->
+       List.map (fun name -> (snd name, Vernacexpr.Implicit)) items
+    | "{"; items = LIST1 name; "}" ->
+       List.map (fun name -> (snd name, Vernacexpr.MaximallyImplicit)) items
+    ]
+  ];
   strategy_level:
     [ [ IDENT "expand" -> Conv_oracle.Expand
       | IDENT "opaque" -> Conv_oracle.Opaque
diff --git a/pretyping/arguments_renaming.ml b/pretyping/arguments_renaming.ml
index ca1d0b7fb..e18aece09 100644
--- a/pretyping/arguments_renaming.ml
+++ b/pretyping/arguments_renaming.ml
@@ -16,12 +16,12 @@ open Libobject
 (*i*)
 
 let name_table =
-  Summary.ref (Refmap.empty : Name.t list list Refmap.t)
+  Summary.ref (Refmap.empty : Name.t list Refmap.t)
     ~name:"rename-arguments"
 
 type req =
   | ReqLocal
-  | ReqGlobal of global_reference * Name.t list list
+  | ReqGlobal of global_reference * Name.t list
 
 let load_rename_args _ (_, (_, (r, names))) =
   name_table := Refmap.add r names !name_table
@@ -49,7 +49,7 @@ let discharge_rename_args = function
        let vars,_,_ = section_segment_of_reference c in
        let c' = pop_global_reference c in
        let var_names = List.map (fun (id, _,_,_) -> Name id) vars in
-       let names' = List.map (fun l -> var_names @ l) names in
+       let names' = var_names @ names in
        Some (ReqGlobal (c', names), (c', names'))
      with Not_found -> Some req)
   | _ -> None
@@ -83,7 +83,7 @@ let rec rename_prod c = function
       | _ -> c
         
 let rename_type ty ref =
-  try rename_prod ty (List.hd (arguments_names ref))
+  try rename_prod ty (arguments_names ref)
   with Not_found -> ty
 
 let rename_type_of_constant env c =
diff --git a/pretyping/arguments_renaming.mli b/pretyping/arguments_renaming.mli
index a33405501..e123e7786 100644
--- a/pretyping/arguments_renaming.mli
+++ b/pretyping/arguments_renaming.mli
@@ -11,10 +11,10 @@ open Globnames
 open Environ
 open Term
 
-val rename_arguments : bool -> global_reference -> Name.t list list -> unit
+val rename_arguments : bool -> global_reference -> Name.t list -> unit
 
-(** [Not_found] is raised is no names are defined for [r] *)
-val arguments_names : global_reference -> Name.t list list
+(** [Not_found] is raised if no names are defined for [r] *)
+val arguments_names : global_reference -> Name.t list
 
 val rename_type_of_constant : env -> pconstant -> types
 val rename_type_of_inductive : env -> pinductive -> types
diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml
index cfb4e79f0..5455ab891 100644
--- a/printing/ppvernac.ml
+++ b/printing/ppvernac.ml
@@ -1023,7 +1023,7 @@ module Make
                      str"[" ++ prlist_with_sep sep pr_explanation imps ++ str"]")
                    impls)
         )
-      | VernacArguments (q, impl, nargs, mods) ->
+      | VernacArguments (q, args, more_implicits, nargs, mods) ->
         return (
           hov 2 (
             keyword "Arguments" ++ spc() ++
@@ -1031,19 +1031,28 @@ module Make
               let pr_s = function None -> str"" | Some (_,s) -> str "%" ++ str s in
               let pr_if b x = if b then x else str "" in
               let pr_br imp x = match imp with
-                | `Implicit -> str "[" ++ x ++ str "]"
-                | `MaximallyImplicit -> str "{" ++ x ++ str "}"
-                | `NotImplicit -> x in
-              let rec aux n l =
+                | Vernacexpr.Implicit -> str "[" ++ x ++ str "]"
+                | Vernacexpr.MaximallyImplicit -> str "{" ++ x ++ str "}"
+                | Vernacexpr.NotImplicit -> x in
+              let rec print_arguments n l =
                 match n, l with
-                  | 0, l -> spc () ++ str"/" ++ aux ~-1 l
+                  | Some 0, l -> spc () ++ str"/" ++ print_arguments None l
                   | _, [] -> mt()
                   | n, { name = id; recarg_like = k;
                          notation_scope = s;
                          implicit_status = imp } :: tl ->
                     spc() ++ pr_br imp (pr_if k (str"!") ++ pr_name id ++ pr_s s) ++
-                      aux (n-1) tl in
-              prlist_with_sep (fun () -> str", ") (aux nargs) impl ++
+                      print_arguments (Option.map pred n) tl
+              in
+              let rec print_implicits = function
+                | [] -> mt ()
+                | (name, impl) :: rest ->
+                   spc() ++ pr_br impl (pr_name name) ++ print_implicits rest
+              in
+              print_arguments nargs args ++
+                if not (List.is_empty more_implicits) then
+                  str ", " ++ prlist_with_sep (fun () -> str", ") print_implicits more_implicits
+                else (mt ()) ++
                 (if not (List.is_empty mods) then str" : " else str"") ++
                   prlist_with_sep (fun () -> str", " ++ spc()) (function
                     | `ReductionDontExposeCase -> keyword "simpl nomatch"
diff --git a/printing/prettyp.ml b/printing/prettyp.ml
index f71719cb9..b590a8c93 100644
--- a/printing/prettyp.ml
+++ b/printing/prettyp.ml
@@ -241,7 +241,7 @@ let print_name_infos ref =
   let impls = implicits_of_global ref in
   let scopes = Notation.find_arguments_scope ref in
   let renames =
-    try List.hd (Arguments_renaming.arguments_names ref) with Not_found -> [] in
+    try Arguments_renaming.arguments_names ref with Not_found -> [] in
   let type_info_for_implicit =
     if need_expansion (select_impargs_size 0 impls) ref then
       (* Need to reduce since implicits are computed with products flattened *)
@@ -281,7 +281,7 @@ let print_inductive_implicit_args =
 let print_inductive_renames =
   print_args_data_of_inductive_ids
     (fun r ->
-      try List.hd (Arguments_renaming.arguments_names r) with Not_found -> [])
+      try Arguments_renaming.arguments_names r with Not_found -> [])
     ((!=) Anonymous)
     print_renames_list
 
diff --git a/test-suite/.csdp.cache b/test-suite/.csdp.cache
index b8c07512f..b99d80e95 100644
--- a/test-suite/.csdp.cache
+++ b/test-suite/.csdp.cache
diff --git a/test-suite/output/Arguments.out b/test-suite/output/Arguments.out
index 2c7b04c62..a2ee2d4c8 100644
--- a/test-suite/output/Arguments.out
+++ b/test-suite/output/Arguments.out
@@ -101,4 +101,4 @@ Error: Unknown interpretation for notation "$".
 w 3 true = tt
      : Prop
 The command has indeed failed with message:
-Error: Extra argument _.
+Error: Extra arguments: _, _.
diff --git a/test-suite/output/Arguments_renaming.out b/test-suite/output/Arguments_renaming.out
index 1633ad976..8c5efcd89 100644
--- a/test-suite/output/Arguments_renaming.out
+++ b/test-suite/output/Arguments_renaming.out
@@ -1,20 +1,12 @@
-File "stdin", line 1, characters 0-36:
-Warning: Ignoring rename of x into y. Only implicit arguments can be renamed.
-[arguments-ignore-rename-nonimpl,vernacular]
 The command has indeed failed with message:
-Error: To rename arguments the "rename" flag must be specified.
+Error: To rename arguments the "rename" flag must be
+specified.
 Argument A renamed to B.
 File "stdin", line 2, characters 0-25:
-Warning: Ignoring rename of A into T. Only implicit arguments can be renamed.
-[arguments-ignore-rename-nonimpl,vernacular]
-File "stdin", line 2, characters 0-25:
-Warning: This command is just asserting the number and names of arguments of
-identity. If this is what you want add ': assert' to silence the warning. If
-you want to clear implicit arguments add ': clear implicits'. If you want to
-clear notation scopes add ': clear scopes' [arguments-assert,vernacular]
-File "stdin", line 4, characters 0-40:
-Warning: Ignoring rename of x into y. Only implicit arguments can be renamed.
-[arguments-ignore-rename-nonimpl,vernacular]
+Warning: This command is just asserting the names of arguments of identity.
+If this is what you want add ': assert' to silence the warning. If you want
+to clear implicit arguments add ': clear implicits'. If you want to clear
+notation scopes add ': clear scopes' [arguments-assert,vernacular]
 @eq_refl
      : forall (B : Type) (y : B), y = y
 eq_refl
@@ -112,18 +104,16 @@ Expands to: Constant Top.myplus
 @myplus
      : forall Z : Type, Z -> nat -> nat -> nat
 The command has indeed failed with message:
-Error: All arguments lists must declare the same names.
+Error: Arguments lists should agree on names they provide.
 The command has indeed failed with message:
-Error: The following arguments are not declared: x.
+Error: Sequences of implicit arguments must be of different lengths
 The command has indeed failed with message:
 Error: Arguments names must be distinct.
 The command has indeed failed with message:
 Error: Argument z cannot be declared implicit.
 The command has indeed failed with message:
-Error: Extra argument y.
-File "stdin", line 53, characters 0-26:
-Warning: Ignoring rename of x into s. Only implicit arguments can be renamed.
-[arguments-ignore-rename-nonimpl,vernacular]
+Error: Extra arguments: y.
 The command has indeed failed with message:
-Error: To rename arguments the "rename" flag must be specified.
+Error: To rename arguments the "rename" flag must be
+specified.
 Argument A renamed to R.
diff --git a/test-suite/output/Arguments_renaming.v b/test-suite/output/Arguments_renaming.v
index e42c98336..2d14c94ac 100644
--- a/test-suite/output/Arguments_renaming.v
+++ b/test-suite/output/Arguments_renaming.v
@@ -1,5 +1,5 @@
 Fail Arguments eq_refl {B y}, [B] y.
-Arguments identity T _ _.
+Arguments identity A _ _.
 Arguments eq_refl A x : assert.
 Arguments eq_refl {B y}, [B] y : rename.
 
@@ -46,9 +46,9 @@ About myplus.
 Check @myplus.
 
 Fail Arguments eq_refl {F g}, [H] k.
-Fail Arguments eq_refl {F}, [F].
+Fail Arguments eq_refl {F}, [F] : rename.
 Fail Arguments eq_refl {F F}, [F] F.
-Fail Arguments eq {F} x [z].
+Fail Arguments eq {F} x [z] : rename.
 Fail Arguments eq {F} x z y.
 Fail Arguments eq {R} s t.
 
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index feec23b50..8a2caa446 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -973,182 +973,255 @@ let vernac_declare_implicits locality r l =
 let warn_arguments_assert =
   CWarnings.create ~name:"arguments-assert" ~category:"vernacular"
          (fun sr ->
-          strbrk "This command is just asserting the number and names of arguments of " ++
+          strbrk "This command is just asserting the names of arguments of " ++
             pr_global sr ++ strbrk". If this is what you want add " ++
             strbrk "': assert' to silence the warning. If you want " ++
             strbrk "to clear implicit arguments add ': clear implicits'. " ++
             strbrk "If you want to clear notation scopes add ': clear scopes'")
-         
-let warn_renaming_nonimplicit =
-  CWarnings.create ~name:"arguments-ignore-rename-nonimpl"
-                   ~category:"vernacular"
-         (fun (oldn, newn) ->
-          strbrk "Ignoring rename of "++pr_id oldn++str" into "++pr_id newn++
-          strbrk ". Only implicit arguments can be renamed.")
-
-let vernac_declare_arguments locality r l nargs flags =
-  let extra_scope_flag = List.mem `ExtraScopes flags in
-  let names = List.map (List.map (fun { name } -> name)) l in
-  let names, rest = List.hd names, List.tl names in
-  let scopes = List.map (List.map (fun { notation_scope = s } -> s)) l in
-  if List.exists (fun na -> not (List.equal Name.equal na names)) rest then
-    error "All arguments lists must declare the same names.";
-  if not (List.distinct_f Name.compare (List.filter ((!=) Anonymous) names))
-  then error "Arguments names must be distinct.";
-  let sr = smart_global r in
+
+(* [nargs_for_red] is the number of arguments required to trigger reduction,
+   [args] is the main list of arguments statuses,
+   [more_implicits] is a list of extra lists of implicit statuses  *)
+let vernac_arguments locality reference args more_implicits nargs_for_red flags =
+  let assert_flag = List.mem `Assert flags in
+  let rename_flag = List.mem `Rename flags in
+  let clear_scopes_flag = List.mem `ClearScopes flags in
+  let extra_scopes_flag = List.mem `ExtraScopes flags in
+  let clear_implicits_flag = List.mem `ClearImplicits flags in
+  let default_implicits_flag = List.mem `DefaultImplicits flags in
+  let never_unfold_flag = List.mem `ReductionNeverUnfold flags in
+
+  let err_incompat x y =
+    error ("Options \""^x^"\" and \""^y^"\" are incompatible.") in
+
+  if assert_flag && rename_flag then
+    err_incompat "assert" "rename";
+  if Option.has_some nargs_for_red && never_unfold_flag then
+    err_incompat "simpl never" "/";
+  if never_unfold_flag && List.mem `ReductionDontExposeCase flags then
+    err_incompat "simpl never" "simpl nomatch";
+  if clear_scopes_flag && extra_scopes_flag then
+    err_incompat "clear scopes" "extra scopes";
+  if clear_implicits_flag && default_implicits_flag then
+    err_incompat "clear implicits" "default implicits";
+
+  let sr = smart_global reference in
   let inf_names =
     let ty = Global.type_of_global_unsafe sr in
-      Impargs.compute_implicits_names (Global.env ()) ty in
-  let rec check li ld ls = match li, ld, ls with
-    | [], [], [] -> ()
-    | [], Anonymous::ld, (Some _)::ls when extra_scope_flag -> check li ld ls
-    | [], _::_, (Some _)::ls when extra_scope_flag ->
-       error "Extra notation scopes can be set on anonymous arguments only"
-    | [], x::_, _ -> errorlabstrm "vernac_declare_arguments"
-                       (str "Extra argument " ++ pr_name x ++ str ".")
-    | l, [], _ -> errorlabstrm "vernac_declare_arguments"
-                    (str "The following arguments are not declared: " ++
-                       prlist_with_sep pr_comma pr_name l ++ str ".")
-    | _::li, _::ld, _::ls -> check li ld ls 
-    | _ -> assert false in
-  let () = match l with
-  | [[]] when List.exists ((<>) `Assert) flags ||
-              (* Arguments f /. used to be allowed by mistake *)
-              (Flags.version_less_or_equal Flags.V8_5 && nargs >= 0) -> ()
-  | _ ->
-    List.iter2 (check inf_names) (names :: rest) scopes
+    Impargs.compute_implicits_names (Global.env ()) ty
   in
-  (* we take extra scopes apart, and we check they are consistent *)
-  let l, scopes = 
-    let scopes, rest = List.hd scopes, List.tl scopes in
-    if List.exists (List.exists ((!=) None)) rest then
-      error "Notation scopes can be given only once";
-    if not extra_scope_flag then l, scopes else
-    let l, _ = List.split (List.map (List.chop (List.length inf_names)) l) in
-    l, scopes in
-  (* we interpret _ as the inferred names *)
-  let l = match l with
-  | [[]] -> l
-  | _ ->
-    let name_anons = function
-      | { name = Anonymous } as x, Name id -> { x with name = Name id }
-      | 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 { name } -> name)) l in
-  let renamed_arg = ref None in
-  let set_renamed a b =
-    if Option.is_empty !renamed_arg && not (Id.equal a b) then
-      renamed_arg := Some(b,a)
+  let prev_names =
+    try Arguments_renaming.arguments_names sr with Not_found -> inf_names
   in
-  let some_renaming_specified =
-    try
-      let names = Arguments_renaming.arguments_names sr in
-      not (List.equal (List.equal Name.equal) names names_decl)
-    with Not_found -> false in
-  let some_renaming_specified, implicits =
-    match l with
-    | [[]] -> false, [[]]
+  let num_args = List.length inf_names in
+  assert (Int.equal num_args (List.length prev_names));
+
+  let names_of args = List.map (fun a -> a.name) args in
+
+  (* Checks *)
+
+  let err_extra_args names =
+    errorlabstrm "vernac_declare_arguments"
+                 (strbrk "Extra arguments: " ++
+                    prlist_with_sep pr_comma pr_name names ++ str ".")
+  in
+  let err_missing_args names =
+    errorlabstrm "vernac_declare_arguments"
+                 (strbrk "The following arguments are not declared: " ++
+                    prlist_with_sep pr_comma pr_name names ++ str ".")
+  in
+
+  let rec check_extra_args extra_args =
+    match extra_args with
+    | [] -> ()
+    | { notation_scope = None } :: _ -> err_extra_args (names_of extra_args)
+    | { name = Anonymous; notation_scope = Some _ } :: args ->
+       check_extra_args args
     | _ ->
-       let some_renaming = ref some_renaming_specified in
-       let rec aux il =
-         match il with
-         | [] -> []
-         | il :: ils -> aux_single il inf_names :: aux ils
-       and aux_single impl inf_names =
-         match impl, inf_names with
-         | [], _ -> []
-         | { name = Anonymous;
-             implicit_status = (`Implicit|`MaximallyImplicit)} :: _,
-           Name id :: _ ->
-             assert false
-         | { name = Name x;
-             implicit_status = (`Implicit|`MaximallyImplicit)} :: _,
-           Anonymous :: _ ->
-             errorlabstrm "vernac_declare_arguments"
-               (str"Argument "++ pr_id x ++str " cannot be declared implicit.")
-         | { name = Name iid;
-             implicit_status = (`Implicit|`MaximallyImplicit as i)} :: impl,
-           Name id :: inf_names ->
-            let max = i = `MaximallyImplicit in
-            set_renamed iid id;
-            some_renaming := !some_renaming || not (Id.equal iid id);
-            (ExplByName id,max,false) :: aux_single impl inf_names
-         | { name = Name iid } :: impl,
-           Name id :: inf_names when not (Id.equal iid id) ->
-            warn_renaming_nonimplicit (id, iid);
-            aux_single impl inf_names
-         | { name = Name iid } :: impl, Name id :: inf_names
-           when not (Id.equal iid id) ->
-            aux_single impl inf_names
-         | { name = Name iid } :: impl, Name id :: inf_names ->
-            set_renamed iid id;
-            some_renaming := !some_renaming || not (Id.equal iid id);
-            aux_single impl inf_names
-         | _ :: impl, _ :: inf_names ->
-            (* no rename, no implicit status *) aux_single impl inf_names
-         | _ :: _, [] -> assert false (* checked before in check() *)
-       in
-       !some_renaming, aux l in
-  (* We check if renamed arguments do match previously declared imp args,
-   * since the system has this invariant *)
-  let some_implicits_specified =
-    match implicits with [[]] -> false | _ -> true in
-  if some_renaming_specified then
-    if not (List.mem `Rename flags) then
-      errorlabstrm "vernac_declare_arguments"
-        (str "To rename arguments the \"rename\" flag must be specified." ++
-           match !renamed_arg with
-           | None -> mt ()
-           | Some (o,n) ->
-              str "\nArgument " ++ pr_id o ++
-              str " renamed to " ++ pr_id n ++ str ".")
-    else
-      Arguments_renaming.rename_arguments
-         (make_section_locality locality) sr names_decl;
-  (* All other infos are in the first item of l *)
-  let l = List.hd l in
-  let scopes = List.map (function
-    | None -> None
-    | Some (o, k) ->
-        try ignore (Notation.find_scope k); Some k
-        with UserError _ ->
-          Some (Notation.find_delimiters_scope o k)) scopes
+       error "Extra notation scopes can be set on anonymous and explicit arguments only."
+  in
+
+  let args, scopes =
+    let scopes = List.map (fun { notation_scope = s } -> s) args in
+    if List.length args > num_args then
+      let args, extra_args = List.chop num_args args in
+      if extra_scopes_flag then
+        (check_extra_args extra_args; (args, scopes))
+      else err_extra_args (names_of extra_args)
+    else args, scopes
+  in
+
+  if Option.cata (fun n -> n > num_args) false nargs_for_red then
+    error "The \"/\" modifier should be put before any extra scope.";
+
+  let scopes_specified = List.exists Option.has_some scopes in
+  
+  if scopes_specified && clear_scopes_flag then
+    error "The \"clear scopes\" flag is incompatible with scope annotations.";
+
+  let names = List.map (fun { name } -> name) args in
+  let names = names :: List.map (List.map fst) more_implicits in
+
+  let rename_flag_required = ref false in
+  let example_renaming = ref None in
+  let save_example_renaming renaming =
+    rename_flag_required := !rename_flag_required
+                            || not (Name.equal (fst renaming) Anonymous);
+    if Option.is_empty !example_renaming then
+      example_renaming := Some renaming
+  in
+
+  let rec names_union names1 names2 =
+    match names1, names2 with
+    | [], [] -> []
+    | _ :: _, [] -> names1
+    | [], _ :: _ -> names2
+    | (Name _ as name) :: names1, Anonymous :: names2
+    | Anonymous :: names1, (Name _ as name) :: names2 ->
+       name :: names_union names1 names2
+    | name1 :: names1, name2 :: names2 ->
+       if Name.equal name1 name2 then
+         name1 :: names_union names1 names2
+       else error "Arguments lists should agree on names they provide."
+  in
+
+  let initial = List.make num_args Anonymous in
+  let names = List.fold_left names_union initial names in
+
+  let rec rename prev_names names =
+    match prev_names, names with
+    | [], [] -> []
+    | [], _ :: _ -> err_extra_args names
+    | _ :: _, [] when assert_flag ->
+       (* Error messages are expressed in terms of original names, not
+            renamed ones. *)
+       err_missing_args (List.lastn (List.length prev_names) inf_names)
+    | _ :: _, [] -> prev_names
+    | prev :: prev_names, Anonymous :: names ->
+       prev :: rename prev_names names
+    | prev :: prev_names, (Name id as name) :: names ->
+       if not (Name.equal prev name) then save_example_renaming (prev,name);
+       name :: rename prev_names names
+  in
+  
+  let names = rename prev_names names in
+  let renaming_specified = Option.has_some !example_renaming in
+
+  if not (List.distinct_f Name.compare (List.filter ((!=) Anonymous) names)) then
+    error "Arguments names must be distinct.";
+
+  if !rename_flag_required && not rename_flag then
+    errorlabstrm "vernac_declare_arguments"
+      (strbrk "To rename arguments the \"rename\" flag must be specified."
+    ++
+       match !example_renaming with
+       | None -> mt ()
+       | Some (o,n) ->
+          str "\nArgument " ++ pr_name o ++
+            str " renamed to " ++ pr_name n ++ str ".");
+
+
+  (* Parts of this code are overly complicated because the implicit arguments
+     API is completely crazy: positions (ExplByPos) are elaborated to
+     names. This is broken by design, since not all arguments have names. So
+     eventhough we eventually want to map only positions to implicit statuses,
+     we have to check whether the corresponding arguments have names, not to
+     trigger an error in the impargs code. Even better, the names we have to
+     check are not the current ones (after previous renamings), but the original
+     ones (inferred from the type). *)
+
+  let implicits =
+    List.map (fun { name; implicit_status = i } -> (name,i)) args
+  in
+  let implicits = implicits :: more_implicits in
+
+  let open Vernacexpr in
+  let rec build_implicits inf_names implicits =
+    match inf_names, implicits with
+    | _, [] -> []
+    | _ :: inf_names, (_, NotImplicit) :: implicits ->
+       build_implicits inf_names implicits
+
+    (* With the current impargs API, it is impossible to make an originally
+       anonymous argument implicit *)
+    | Anonymous :: _, (name, _) :: _ ->
+       errorlabstrm "vernac_declare_arguments"
+                    (strbrk"Argument "++ pr_name name ++ 
+                       strbrk " cannot be declared implicit.")
+
+    | Name id :: inf_names, (name, impl) :: implicits ->
+       let max = impl = MaximallyImplicit in
+       (ExplByName id,max,false) :: build_implicits inf_names implicits
+    
+    | _ -> assert false (* already checked in [names_union] *)
   in
-  let some_scopes_specified = List.exists ((!=) None) scopes in
+  
+  let implicits = List.map (build_implicits inf_names) implicits in
+  let implicits_specified = match implicits with [[]] -> false | _ -> true in
+
+  if implicits_specified && clear_implicits_flag then
+    error "The \"clear implicits\" flag is incompatible with implicit annotations";
+
+  if implicits_specified && default_implicits_flag then
+    error "The \"default implicits\" flag is incompatible with implicit annotations";
+
   let rargs =
     Util.List.map_filter (function (n, true) -> Some n | _ -> None)
-      (Util.List.map_i (fun i { recarg_like = b } -> i, b) 0 l) in
-  if some_scopes_specified || List.mem `ClearScopes flags then
-    vernac_arguments_scope locality r scopes;
-  if not some_implicits_specified && List.mem `DefaultImplicits flags then
-    vernac_declare_implicits locality r []
-  else if some_implicits_specified || List.mem `ClearImplicits flags then
-    vernac_declare_implicits locality r implicits;
-  if nargs >= 0 && nargs <= List.fold_left max ~-1 rargs then
-    error "The \"/\" option must be placed after the last \"!\".";
-  let no_flags = List.is_empty flags in
+      (Util.List.map_i (fun i { recarg_like = b } -> i, b) 0 args)
+  in
+
   let rec narrow = function
     | #Reductionops.ReductionBehaviour.flag as x :: tl -> x :: narrow tl
-    | [] -> [] | _ :: tl -> narrow tl in
-  let flags = narrow flags in
-  let some_simpl_flags_specified =
-    not (List.is_empty rargs) || nargs >= 0 || not (List.is_empty flags) in
-  if some_simpl_flags_specified then begin
+    | [] -> [] | _ :: tl -> narrow tl
+  in
+  let red_flags = narrow flags in
+  let red_modifiers_specified =
+    not (List.is_empty rargs) || Option.has_some nargs_for_red
+    || not (List.is_empty red_flags)
+  in
+
+  if not (List.is_empty rargs) && never_unfold_flag then
+    err_incompat "simpl never" "!";
+
+
+  (* Actions *)
+
+  if renaming_specified then begin
+    let local = make_section_locality locality in
+    Arguments_renaming.rename_arguments local sr names
+  end;
+
+  if scopes_specified || clear_scopes_flag then begin
+      let scopes = List.map (Option.map (fun (o,k) -> 
+        try ignore (Notation.find_scope k); k
+        with UserError _ ->
+          Notation.find_delimiters_scope o k)) scopes
+      in
+      vernac_arguments_scope locality reference scopes
+    end;
+
+  if implicits_specified || clear_implicits_flag then
+    vernac_declare_implicits locality reference implicits;
+
+  if default_implicits_flag then
+    vernac_declare_implicits locality reference [];
+
+  if red_modifiers_specified then begin
     match sr with
     | ConstRef _ as c ->
        Reductionops.ReductionBehaviour.set
-         (make_section_locality locality) c (rargs, nargs, flags)
+         (make_section_locality locality) c
+         (rargs, Option.default ~-1 nargs_for_red, red_flags)
     | _ -> errorlabstrm ""
              (strbrk "Modifiers of the behavior of the simpl tactic "++
               strbrk "are relevant for constants only.")
   end;
-  if not (some_renaming_specified ||
-          some_implicits_specified ||
-          some_scopes_specified ||
-          some_simpl_flags_specified) &&
-     no_flags then
-    warn_arguments_assert sr
 
+ if not (renaming_specified ||
+         implicits_specified ||
+         scopes_specified ||
+         red_modifiers_specified) && (List.is_empty flags) then
+    warn_arguments_assert sr
 
 let default_env () = {
   Notation_term.ninterp_var_type = Id.Map.empty;
@@ -1920,8 +1993,8 @@ let interp ?proof ~loc locality poly c =
       vernac_syntactic_definition locality  id c local b
   | VernacDeclareImplicits (qid,l) ->
       vernac_declare_implicits locality qid l
-  | VernacArguments (qid, l, narg, flags) ->
-      vernac_declare_arguments locality qid l narg flags 
+  | VernacArguments (qid, args, more_implicits, nargs, flags) ->
+      vernac_arguments locality qid args more_implicits nargs flags
   | VernacReserve bl -> vernac_reserve bl
   | VernacGeneralizable gen -> vernac_generalizable locality gen
   | VernacSetOpacity qidl -> vernac_set_opacity locality qidl