Move Arguments implementation to its own file (from vernacentries)

5 files changed, 346 insertions, 298 deletions

diff --git a/vernac/comArguments.ml b/vernac/comArguments.ml
new file mode 100644
index 0000000000..737e0427ec
--- /dev/null
+++ b/vernac/comArguments.ml
@@ -0,0 +1,306 @@
+(************************************************************************)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2019       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
+(*   \VV/  **************************************************************)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
+(************************************************************************)
+
+open CAst
+open Util
+open Names
+open Vernacexpr
+
+let smart_global r =
+  let gr = Smartlocate.smart_global r in
+  Dumpglob.add_glob ?loc:r.loc gr;
+  gr
+
+let cache_bidi_hints (_name, (gr, ohint)) =
+  match ohint with
+  | None -> Pretyping.clear_bidirectionality_hint gr
+  | Some nargs -> Pretyping.add_bidirectionality_hint gr nargs
+
+let load_bidi_hints _ r =
+  cache_bidi_hints r
+
+let subst_bidi_hints (subst, (gr, ohint as orig)) =
+  let gr' = Globnames.subst_global_reference subst gr in
+  if gr == gr' then orig else (gr', ohint)
+
+let discharge_bidi_hints (_name, (gr, ohint)) =
+  if Globnames.isVarRef gr && Lib.is_in_section gr then None
+  else
+    let vars = Lib.variable_section_segment_of_reference gr in
+    let n = List.length vars in
+    Some (gr, Option.map ((+) n) ohint)
+
+let inBidiHints =
+  let open Libobject in
+  declare_object { (default_object "BIDIRECTIONALITY-HINTS" ) with
+                   load_function = load_bidi_hints;
+                   cache_function = cache_bidi_hints;
+                   classify_function = (fun o -> Substitute o);
+                   subst_function = subst_bidi_hints;
+                   discharge_function = discharge_bidi_hints;
+                 }
+
+
+let warn_arguments_assert =
+  CWarnings.create ~name:"arguments-assert" ~category:"vernacular"
+    Pp.(fun sr ->
+        strbrk "This command is just asserting the names of arguments of " ++
+        Printer.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'")
+
+(* [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 ~section_local reference args more_implicits nargs_for_red nargs_before_bidi flags =
+  let env = Global.env () in
+  let sigma = Evd.from_env env in
+  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 nomatch_flag = List.mem `ReductionDontExposeCase flags in
+  let clear_bidi_hint = List.mem `ClearBidiHint flags in
+
+  let err_incompat x y =
+    CErrors.user_err Pp.(str ("Options \""^x^"\" and \""^y^"\" are incompatible.")) in
+
+  if assert_flag && rename_flag then
+    err_incompat "assert" "rename";
+  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, _ = Typeops.type_of_global_in_context env sr in
+    Impargs.compute_implicits_names env sigma (EConstr.of_constr ty)
+  in
+  let prev_names =
+    try Arguments_renaming.arguments_names sr with Not_found -> inf_names
+  in
+  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 =
+    CErrors.user_err ~hdr:"vernac_declare_arguments"
+      Pp.(strbrk "Extra arguments: " ++
+          prlist_with_sep pr_comma Name.print names ++ str ".")
+  in
+  let err_missing_args names =
+    CErrors.user_err ~hdr:"vernac_declare_arguments"
+      Pp.(strbrk "The following arguments are not declared: " ++
+          prlist_with_sep pr_comma Name.print names ++ str ".")
+  in
+
+  let rec check_extra_args extra_args =
+    match extra_args with
+    | [] -> ()
+    | { notation_scope = None } :: _ ->
+      CErrors.user_err Pp.(str"Extra arguments should specify a scope.")
+    | { notation_scope = Some _ } :: args -> check_extra_args args
+  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
+    CErrors.user_err Pp.(str "The \"/\" modifier should be put before any extra scope.");
+
+  if Option.cata (fun n -> n > num_args) false nargs_before_bidi then
+    CErrors.user_err Pp.(str "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
+    CErrors.user_err Pp.(str "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 CErrors.user_err Pp.(str "Argument lists should agree on the names they provide.")
+  in
+
+  let names = List.fold_left names_union [] 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 !rename_flag_required && not rename_flag then begin
+    let msg = let open Pp in
+      match !example_renaming with
+      | None ->
+        strbrk "To rename arguments the \"rename\" flag must be specified."
+      | Some (o,n) ->
+        strbrk "Flag \"rename\" expected to rename " ++ Name.print o ++
+        strbrk " into " ++ Name.print n ++ str "."
+    in CErrors.user_err ~hdr:"vernac_declare_arguments" msg
+  end;
+
+  let duplicate_names =
+    List.duplicates Name.equal (List.filter ((!=) Anonymous) names)
+  in
+  if not (List.is_empty duplicate_names) then begin
+    CErrors.user_err Pp.(strbrk "Some argument names are duplicated: " ++
+                         prlist_with_sep pr_comma Name.print duplicate_names)
+  end;
+
+  let implicits =
+    List.map (fun { name; implicit_status = i } -> (name,i)) args
+  in
+  let implicits = implicits :: more_implicits in
+
+  let implicits = List.map (List.map snd) implicits in
+  let implicits_specified = match implicits with
+    | [l] -> List.exists (function Impargs.NotImplicit -> false | _ -> true) l
+    | _ -> true in
+
+  if implicits_specified && clear_implicits_flag then
+    CErrors.user_err Pp.(str "The \"clear implicits\" flag is incompatible with implicit annotations");
+
+  if implicits_specified && default_implicits_flag then
+    CErrors.user_err Pp.(str "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 args)
+  in
+
+  let red_behavior =
+    let open Reductionops.ReductionBehaviour in
+    match never_unfold_flag, nomatch_flag, rargs, nargs_for_red with
+    | true, false, [], None -> Some NeverUnfold
+    | true, true, _, _ -> err_incompat "simpl never" "simpl nomatch"
+    | true, _, _::_, _ -> err_incompat "simpl never" "!"
+    | true, _, _, Some _ -> err_incompat "simpl never" "/"
+    | false, false, [], None  -> None
+    | false, false, _, _ -> Some (UnfoldWhen { nargs = nargs_for_red;
+                                               recargs = rargs;
+                                             })
+    | false, true, _, _ -> Some (UnfoldWhenNoMatch { nargs = nargs_for_red;
+                                                     recargs = rargs;
+                                                   })
+  in
+
+
+  let red_modifiers_specified = Option.has_some red_behavior in
+
+  let bidi_hint_specified = Option.has_some nargs_before_bidi in
+
+  if bidi_hint_specified && clear_bidi_hint then
+    err_incompat "clear bidirectionality hint" "&";
+
+
+  (* Actions *)
+
+  if renaming_specified then begin
+    Arguments_renaming.rename_arguments section_local sr names
+  end;
+
+  if scopes_specified || clear_scopes_flag then begin
+    let scopes = List.map (Option.map (fun {loc;v=k} ->
+        try ignore (Notation.find_scope k); k
+        with CErrors.UserError _ ->
+          Notation.find_delimiters_scope ?loc k)) scopes
+    in
+    Notation.declare_arguments_scope section_local (smart_global reference) scopes
+  end;
+
+  if implicits_specified || clear_implicits_flag then
+    Impargs.set_implicits section_local (smart_global reference) implicits;
+
+  if default_implicits_flag then
+    Impargs.declare_implicits section_local (smart_global reference);
+
+  if red_modifiers_specified then begin
+    match sr with
+    | GlobRef.ConstRef _ ->
+      Reductionops.ReductionBehaviour.set
+        ~local:section_local sr (Option.get red_behavior)
+
+    | _ ->
+      CErrors.user_err
+        Pp.(strbrk "Modifiers of the behavior of the simpl tactic "++
+            strbrk "are relevant for constants only.")
+  end;
+
+  if bidi_hint_specified then begin
+    let n = Option.get nargs_before_bidi in
+    if section_local then
+      Pretyping.add_bidirectionality_hint sr n
+    else
+      Lib.add_anonymous_leaf (inBidiHints (sr, Some n))
+  end;
+
+  if clear_bidi_hint then begin
+    if section_local then
+      Pretyping.clear_bidirectionality_hint sr
+    else
+      Lib.add_anonymous_leaf (inBidiHints (sr, None))
+  end;
+
+  if not (renaming_specified ||
+          implicits_specified ||
+          scopes_specified ||
+          red_modifiers_specified ||
+          bidi_hint_specified) && (List.is_empty flags) then
+    warn_arguments_assert sr
diff --git a/vernac/comArguments.mli b/vernac/comArguments.mli
new file mode 100644
index 0000000000..f78e01a11f
--- /dev/null
+++ b/vernac/comArguments.mli
@@ -0,0 +1,19 @@
+(************************************************************************)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2019       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
+(*   \VV/  **************************************************************)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
+(************************************************************************)
+
+val vernac_arguments
+  : section_local:bool
+  -> Libnames.qualid Constrexpr.or_by_notation
+  -> Vernacexpr.vernac_argument_status list
+  -> (Names.Name.t * Impargs.implicit_kind) list list
+  -> int option
+  -> int option
+  -> Vernacexpr.arguments_modifier list
+  -> unit
diff --git a/vernac/vernac.mllib b/vernac/vernac.mllib
index 956b56e256..102da20257 100644
--- a/vernac/vernac.mllib
+++ b/vernac/vernac.mllib
@@ -38,6 +38,7 @@ Assumptions
 Mltop
 Topfmt
 Loadpath
+ComArguments
 Vernacentries
 Vernacstate
 Vernacinterp
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 684d8a3d90..4c7332f011 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -15,7 +15,6 @@ open CErrors
 open CAst
 open Util
 open Names
-open Nameops
 open Tacmach
 open Constrintern
 open Prettyp
@@ -448,9 +447,6 @@ let vernac_bind_scope ~module_local sc cll =
 let vernac_open_close_scope ~section_local (b,s) =
   Notation.open_close_scope (section_local,b,s)
 
-let vernac_arguments_scope ~section_local r scl =
-  Notation.declare_arguments_scope section_local (smart_global r) scl
-
 let vernac_infix ~atts =
   let module_local, deprecation = Attributes.(parse Notations.(module_locality ++ deprecation) atts) in
   Metasyntax.add_infix ~local:module_local deprecation (Global.env())
@@ -655,7 +651,7 @@ let vernac_record ~template udecl cum k poly finite records =
   let cumulative = should_treat_as_cumulative cum poly in
   let map ((coe, id), binders, sort, nameopt, cfs) =
     let const = match nameopt with
-    | None -> add_prefix "Build_" id.v
+    | None -> Nameops.add_prefix "Build_" id.v
     | Some lid ->
       let () = Dumpglob.dump_definition lid false "constr" in
       lid.v
@@ -1213,292 +1209,6 @@ let vernac_syntactic_definition ~atts lid x compat =
   Dumpglob.dump_definition lid false "syndef";
   Metasyntax.add_syntactic_definition ~local:module_local deprecation (Global.env()) lid.v x compat
 
-let cache_bidi_hints (_name, (gr, ohint)) =
-  match ohint with
-  | None -> Pretyping.clear_bidirectionality_hint gr
-  | Some nargs -> Pretyping.add_bidirectionality_hint gr nargs
-
-let load_bidi_hints _ r =
-  cache_bidi_hints r
-
-let subst_bidi_hints (subst, (gr, ohint as orig)) =
-  let gr' = subst_global_reference subst gr in
-  if gr == gr' then orig else (gr', ohint)
-
-let discharge_bidi_hints (_name, (gr, ohint)) =
-  if isVarRef gr && Lib.is_in_section gr then None
-  else
-    let vars = Lib.variable_section_segment_of_reference gr in
-    let n = List.length vars in
-    Some (gr, Option.map ((+) n) ohint)
-
-let inBidiHints =
-  let open Libobject in
-  declare_object { (default_object "BIDIRECTIONALITY-HINTS" ) with
-                   load_function = load_bidi_hints;
-                   cache_function = cache_bidi_hints;
-                   classify_function = (fun o -> Substitute o);
-                   subst_function = subst_bidi_hints;
-                   discharge_function = discharge_bidi_hints;
-                 }
-
-
-let warn_arguments_assert =
-  CWarnings.create ~name:"arguments-assert" ~category:"vernacular"
-         (fun sr ->
-          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'")
-
-(* [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 ~section_local reference args more_implicits nargs_for_red nargs_before_bidi flags =
-  let env = Global.env () in
-  let sigma = Evd.from_env env in
-  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 nomatch_flag = List.mem `ReductionDontExposeCase flags in
-  let clear_bidi_hint = List.mem `ClearBidiHint flags in
-
-  let err_incompat x y =
-    user_err Pp.(str ("Options \""^x^"\" and \""^y^"\" are incompatible.")) in
-
-  if assert_flag && rename_flag then
-    err_incompat "assert" "rename";
-  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, _ = Typeops.type_of_global_in_context env sr in
-    Impargs.compute_implicits_names env sigma (EConstr.of_constr ty)
-  in
-  let prev_names =
-    try Arguments_renaming.arguments_names sr with Not_found -> inf_names
-  in
-  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 =
-    user_err ~hdr:"vernac_declare_arguments"
-                 (strbrk "Extra arguments: " ++
-                    prlist_with_sep pr_comma Name.print names ++ str ".")
-  in
-  let err_missing_args names =
-    user_err ~hdr:"vernac_declare_arguments"
-                 (strbrk "The following arguments are not declared: " ++
-                    prlist_with_sep pr_comma Name.print names ++ str ".")
-  in
-
-  let rec check_extra_args extra_args =
-    match extra_args with
-    | [] -> ()
-    | { notation_scope = None } :: _ ->
-      user_err Pp.(str"Extra arguments should specify a scope.")
-    | { notation_scope = Some _ } :: args -> check_extra_args args
-  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
-    user_err Pp.(str "The \"/\" modifier should be put before any extra scope.");
-
-  if Option.cata (fun n -> n > num_args) false nargs_before_bidi then
-    user_err Pp.(str "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
-    user_err Pp.(str "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 user_err Pp.(str "Argument lists should agree on the names they provide.")
-  in
-
-  let names = List.fold_left names_union [] 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 !rename_flag_required && not rename_flag then begin
-    let msg =
-      match !example_renaming with
-      | None ->
-        strbrk "To rename arguments the \"rename\" flag must be specified."
-      | Some (o,n) ->
-        strbrk "Flag \"rename\" expected to rename " ++ Name.print o ++
-        strbrk " into " ++ Name.print n ++ str "."
-    in user_err ~hdr:"vernac_declare_arguments" msg
-  end;
-
-  let duplicate_names =
-    List.duplicates Name.equal (List.filter ((!=) Anonymous) names)
-  in
-  if not (List.is_empty duplicate_names) then begin
-    let duplicates = prlist_with_sep pr_comma Name.print duplicate_names in
-    user_err (strbrk "Some argument names are duplicated: " ++ duplicates)
-  end;
-
-  let implicits =
-    List.map (fun { name; implicit_status = i } -> (name,i)) args
-  in
-  let implicits = implicits :: more_implicits in
-
-  let implicits = List.map (List.map snd) implicits in
-  let implicits_specified = match implicits with
-    | [l] -> List.exists (function Impargs.NotImplicit -> false | _ -> true) l
-    | _ -> true in
-
-  if implicits_specified && clear_implicits_flag then
-    user_err Pp.(str "The \"clear implicits\" flag is incompatible with implicit annotations");
-
-  if implicits_specified && default_implicits_flag then
-    user_err Pp.(str "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 args)
-  in
-
-  let red_behavior =
-    let open Reductionops.ReductionBehaviour in
-    match never_unfold_flag, nomatch_flag, rargs, nargs_for_red with
-    | true, false, [], None -> Some NeverUnfold
-    | true, true, _, _ -> err_incompat "simpl never" "simpl nomatch"
-    | true, _, _::_, _ -> err_incompat "simpl never" "!"
-    | true, _, _, Some _ -> err_incompat "simpl never" "/"
-    | false, false, [], None  -> None
-    | false, false, _, _ -> Some (UnfoldWhen { nargs = nargs_for_red;
-                                               recargs = rargs;
-                                             })
-    | false, true, _, _ -> Some (UnfoldWhenNoMatch { nargs = nargs_for_red;
-                                                     recargs = rargs;
-                                                   })
-  in
-
-
-  let red_modifiers_specified = Option.has_some red_behavior in
-
-  let bidi_hint_specified = Option.has_some nargs_before_bidi in
-
-  if bidi_hint_specified && clear_bidi_hint then
-    err_incompat "clear bidirectionality hint" "&";
-
-
-  (* Actions *)
-
-  if renaming_specified then begin
-    Arguments_renaming.rename_arguments section_local sr names
-  end;
-
-  if scopes_specified || clear_scopes_flag then begin
-      let scopes = List.map (Option.map (fun {loc;v=k} ->
-        try ignore (Notation.find_scope k); k
-        with UserError _ ->
-          Notation.find_delimiters_scope ?loc k)) scopes
-      in
-      vernac_arguments_scope ~section_local reference scopes
-    end;
-
-  if implicits_specified || clear_implicits_flag then
-    Impargs.set_implicits section_local (smart_global reference) implicits;
-
-  if default_implicits_flag then
-    Impargs.declare_implicits section_local (smart_global reference);
-
-  if red_modifiers_specified then begin
-    match sr with
-    | GlobRef.ConstRef _ as c ->
-       Reductionops.ReductionBehaviour.set
-         ~local:section_local c (Option.get red_behavior)
-
-    | _ -> user_err
-             (strbrk "Modifiers of the behavior of the simpl tactic "++
-              strbrk "are relevant for constants only.")
-  end;
-
-  if bidi_hint_specified then begin
-    let n = Option.get nargs_before_bidi in
-    if section_local then
-      Pretyping.add_bidirectionality_hint sr n
-    else
-      Lib.add_anonymous_leaf (inBidiHints (sr, Some n))
-    end;
-
-  if clear_bidi_hint then begin
-    if section_local then
-      Pretyping.clear_bidirectionality_hint sr
-    else
-      Lib.add_anonymous_leaf (inBidiHints (sr, None))
-  end;
-
- if not (renaming_specified ||
-         implicits_specified ||
-         scopes_specified ||
-         red_modifiers_specified ||
-         bidi_hint_specified) && (List.is_empty flags) then
-    warn_arguments_assert sr
-
 let default_env () = {
   Notation_term.ninterp_var_type = Id.Map.empty;
   ninterp_rec_vars = Id.Map.empty;
@@ -2453,7 +2163,8 @@ let translate_vernac ~atts v = let open Vernacextend in match v with
      VtDefault(fun () -> vernac_syntactic_definition ~atts id c b)
   | VernacArguments (qid, args, more_implicits, nargs, bidi, flags) ->
     VtDefault(fun () ->
-        with_section_locality ~atts (vernac_arguments qid args more_implicits nargs bidi flags))
+        with_section_locality ~atts
+          (ComArguments.vernac_arguments qid args more_implicits nargs bidi flags))
   | VernacReserve bl ->
     VtDefault(fun () ->
         unsupported_attributes atts;
diff --git a/vernac/vernacexpr.ml b/vernac/vernacexpr.ml
index b712d7e264..564c55670d 100644
--- a/vernac/vernacexpr.ml
+++ b/vernac/vernacexpr.ml
@@ -257,6 +257,17 @@ type vernac_argument_status = {
   implicit_status : Impargs.implicit_kind;
 }
 
+type arguments_modifier =
+  [  `Assert
+  | `ClearBidiHint
+  | `ClearImplicits
+  | `ClearScopes
+  | `DefaultImplicits
+  | `ExtraScopes
+  | `ReductionDontExposeCase
+  | `ReductionNeverUnfold
+  | `Rename ]
+
 type extend_name =
   (* Name of the vernac entry where the tactic is defined, typically found
      after the VERNAC EXTEND statement in the source. *)
@@ -365,16 +376,16 @@ type nonrec vernac_expr =
   | VernacCreateHintDb of string * bool
   | VernacRemoveHints of string list * qualid list
   | VernacHints of string list * Hints.hints_expr
-  | VernacSyntacticDefinition of lident * (Id.t list * constr_expr) *
+  | VernacSyntacticDefinition of
+      lident * (Id.t list * constr_expr) *
       onlyparsing_flag
-  | VernacArguments of qualid or_by_notation *
+  | VernacArguments of
+      qualid or_by_notation *
       vernac_argument_status list (* Main arguments status list *) *
-        (Name.t * Impargs.implicit_kind) list list (* Extra implicit status lists *) *
+      (Name.t * Impargs.implicit_kind) list list (* Extra implicit status lists *) *
       int option (* Number of args to trigger reduction *) *
       int option (* Number of args before bidirectional typing *) *
-        [ `ReductionDontExposeCase | `ReductionNeverUnfold | `Rename |
-          `ExtraScopes | `Assert | `ClearImplicits | `ClearScopes | `ClearBidiHint |
-          `DefaultImplicits ] list
+      arguments_modifier list
   | VernacReserve of simple_binder list
   | VernacGeneralizable of (lident list) option
   | VernacSetOpacity of (Conv_oracle.level * qualid or_by_notation list)