Creating a module Nameops.Name extending module Names.Name.

This module collects the functions of Nameops which are about Name.t
and somehow standardize or improve their name, resulting in particular
from discussions in working group.

Note the use of a dedicated exception rather than a failwith for
Nameops.Name.out.

Drawback of the approach: one needs to open Nameops, or to use long
prefix Nameops.Name.

3 files changed, 9 insertions, 9 deletions

diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml
index f76555b04..60511d913 100644
--- a/printing/ppconstr.ml
+++ b/printing/ppconstr.ml
@@ -151,8 +151,8 @@ let tag_var = tag Tag.variable
 
   let pr_univ l =
     match l with
-      | [_,x] -> pr_name x
-      | l -> str"max(" ++ prlist_with_sep (fun () -> str",") (fun x -> pr_name (snd x)) l ++ str")"
+      | [_,x] -> Name.print x
+      | l -> str"max(" ++ prlist_with_sep (fun () -> str",") (fun x -> Name.print (snd x)) l ++ str")"
 
   let pr_univ_annot pr x = str "@{" ++ pr x ++ str "}"
 
@@ -166,7 +166,7 @@ let tag_var = tag Tag.variable
     | GProp -> tag_type (str "Prop")
     | GSet -> tag_type (str "Set")
     | GType None -> tag_type (str "Type")
-    | GType (Some (_, u)) -> tag_type (pr_name u)
+    | GType (Some (_, u)) -> tag_type (Name.print u)
 
   let pr_qualid sp =
     let (sl, id) = repr_qualid sp in
@@ -191,7 +191,7 @@ let tag_var = tag Tag.variable
       tag_type (str "Set")
     | GType u ->
       (match u with
-        | Some (_,u) -> pr_name u
+        | Some (_,u) -> Name.print u
         | None -> tag_type (str "Type"))
 
   let pr_universe_instance l =
@@ -224,7 +224,7 @@ let tag_var = tag Tag.variable
 
   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_or_var pr = function
     | ArgArg x -> pr x
diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml
index c328b6032..6aa136b60 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
diff --git a/printing/prettyp.ml b/printing/prettyp.ml
index 0f7da3613..2b21b3f9e 100644
--- a/printing/prettyp.ml
+++ b/printing/prettyp.ml
@@ -132,7 +132,7 @@ let print_impargs_list prefix l =
 let print_renames_list prefix l =
   if List.is_empty l then [] else
   [add_colon prefix ++ str "Arguments are renamed to " ++
-    hv 2 (prlist_with_sep pr_comma (fun x -> x) (List.map pr_name l))]
+    hv 2 (prlist_with_sep pr_comma (fun x -> x) (List.map Name.print l))]
 
 let need_expansion impl ref =
   let typ = Global.type_of_global_unsafe ref in