Merge remote-tracking branch 'github/pr/337' into v8.6

Was PR#337: Fix arguments

2 files changed, 19 insertions, 10 deletions

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