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.

2 files changed, 19 insertions, 10 deletions

diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml
index cfb4e79f03..5455ab891a 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 f71719cb9a..b590a8c930 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