diff options
| author | Maxime Dénès | 2017-06-01 15:44:11 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2017-06-01 15:44:11 +0200 |
| commit | 84d49e38a245cbbbe5b6111a4e4d9afcbac2d33b (patch) | |
| tree | 0e6bff9cf7c2aaf6967352bd5b5f8c8a2831a570 /printing/ppvernac.ml | |
| parent | 48621da27d52be4825eea271d44bbd7362011dfa (diff) | |
| parent | 8ab00e5f272aa8f16d70a00323c57f2d4ef66f03 (diff) | |
Merge PR#561: Improving the Name API
Diffstat (limited to 'printing/ppvernac.ml')
| -rw-r--r-- | printing/ppvernac.ml | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml index c328b6032b..6aa136b606 100644 --- a/printing/ppvernac.ml +++ b/printing/ppvernac.ml @@ -56,7 +56,7 @@ open Decl_kinds let pr_lname = function | (loc,Name id) -> pr_lident (loc,id) - | lna -> pr_located pr_name lna + | lna -> pr_located Name.print lna let pr_smart_global = Pputils.pr_or_by_notation pr_reference @@ -1022,13 +1022,13 @@ open Decl_kinds | 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) ++ + spc() ++ pr_br imp (pr_if k (str"!") ++ Name.print id ++ pr_s s) ++ 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 + spc() ++ pr_br impl (Name.print name) ++ print_implicits rest in print_arguments nargs args ++ if not (List.is_empty more_implicits) then |