diff options
Diffstat (limited to 'parsing/ppvernac.ml')
| -rw-r--r-- | parsing/ppvernac.ml | 25 |
1 files changed, 25 insertions, 0 deletions
diff --git a/parsing/ppvernac.ml b/parsing/ppvernac.ml index 6254d345f..4e73b3793 100644 --- a/parsing/ppvernac.ml +++ b/parsing/ppvernac.ml @@ -835,6 +835,31 @@ let rec pr_vernac = function prlist_with_sep spc (fun imps -> str"[" ++ prlist_with_sep sep pr_explanation imps ++ str"]") impls) + | VernacArguments (local, q, impl, nargs, mods) -> + hov 2 (pr_section_locality local ++ str"Arguments" ++ spc() ++ + pr_smart_global q ++ + 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 max x = match imp, max with + | true, false -> str "[" ++ x ++ str "]" + | true, true -> str "{" ++ x ++ str "}" + | _ -> x in + let rec aux n l = + match n, l with + | 0, l -> spc () ++ str"/" ++ aux ~-1 l + | _, [] -> mt() + | n, (id,k,s,imp,max) :: tl -> + spc() ++ pr_br imp max (pr_if k (str"!") ++ pr_name id ++ pr_s s) ++ + aux (n-1) tl in + prlist_with_sep (fun () -> str", ") (aux nargs) impl ++ + if mods <> [] then str" : " else str"" ++ + prlist_with_sep (fun () -> str", " ++ spc()) (function + | `SimplDontExposeCase -> str "simpl nomatch" + | `SimplNeverUnfold -> str "simpl never" + | `DefaultImplicits -> str "default implicits" + | `ClearImplicits -> str "clear implicits" + | `ClearScopes -> str "clear scopes") + mods) | VernacReserve bl -> let n = List.length (List.flatten (List.map fst bl)) in hov 2 (str"Implicit Type" ++ |