diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-10-29 16:11:00 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-10-29 16:11:00 +0200 |
| commit | cd1adfe2d51d05381a1044fb5a0086c608184ca9 (patch) | |
| tree | 7a0828ac04b56ce7d764a10b339813cc95a6034d /printing | |
| parent | ebc07e5741fab0df15a8de56fc69397a7d164ce9 (diff) | |
| parent | b5d88066acbcebf598474e0d854b16078f4019ce (diff) | |
Merge branch 'v8.6'
Diffstat (limited to 'printing')
| -rw-r--r-- | printing/ppvernac.ml | 25 | ||||
| -rw-r--r-- | printing/prettyp.ml | 4 |
2 files changed, 19 insertions, 10 deletions
diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml index 5d7249aff..93c3179bc 100644 --- a/printing/ppvernac.ml +++ b/printing/ppvernac.ml @@ -1021,7 +1021,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() ++ @@ -1029,19 +1029,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 3d0b07a1e..b19f8376c 100644 --- a/printing/prettyp.ml +++ b/printing/prettyp.ml @@ -243,7 +243,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 *) @@ -283,7 +283,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 |