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.

4 files changed, 15 insertions, 15 deletions

diff --git a/vernac/auto_ind_decl.ml b/vernac/auto_ind_decl.ml
index cf534f13a2..b99ccbf4a2 100644
--- a/vernac/auto_ind_decl.ml
+++ b/vernac/auto_ind_decl.ml
@@ -533,7 +533,7 @@ open Namegen
 let compute_bl_goal ind lnamesparrec nparrec =
   let eqI, eff = eqI ind lnamesparrec in
   let list_id = list_id lnamesparrec in
-  let avoid = List.fold_right (Nameops.name_fold (fun id l -> id::l)) (List.map RelDecl.get_name lnamesparrec) [] in
+  let avoid = List.fold_right (Nameops.Name.fold_right (fun id l -> id::l)) (List.map RelDecl.get_name lnamesparrec) [] in
   let create_input c =
     let x = next_ident_away (Id.of_string "x") avoid and
         y = next_ident_away (Id.of_string "y") avoid in
@@ -676,7 +676,7 @@ let _ = bl_scheme_kind_aux := fun () -> bl_scheme_kind
 let compute_lb_goal ind lnamesparrec nparrec =
   let list_id = list_id lnamesparrec in
   let eq = Lazy.force eq and tt = Lazy.force tt and bb = Lazy.force bb in
-  let avoid = List.fold_right (Nameops.name_fold (fun id l -> id::l)) (List.map RelDecl.get_name lnamesparrec) [] in
+  let avoid = List.fold_right (Nameops.Name.fold_right (fun id l -> id::l)) (List.map RelDecl.get_name lnamesparrec) [] in
   let eqI, eff = eqI ind lnamesparrec in
     let create_input c =
       let x = next_ident_away (Id.of_string "x") avoid and
@@ -806,7 +806,7 @@ let compute_dec_goal ind lnamesparrec nparrec =
   check_not_is_defined ();
   let eq = Lazy.force eq and tt = Lazy.force tt and bb = Lazy.force bb in
   let list_id = list_id lnamesparrec in
-  let avoid = List.fold_right (Nameops.name_fold (fun id l -> id::l)) (List.map RelDecl.get_name lnamesparrec) [] in
+  let avoid = List.fold_right (Nameops.Name.fold_right (fun id l -> id::l)) (List.map RelDecl.get_name lnamesparrec) [] in
     let create_input c =
       let x = next_ident_away (Id.of_string "x") avoid and
           y = next_ident_away (Id.of_string "y") avoid in
diff --git a/vernac/command.ml b/vernac/command.ml
index e2ebb4d7fb..6ece585a9e 100644
--- a/vernac/command.ml
+++ b/vernac/command.ml
@@ -411,8 +411,8 @@ let mk_mltype_data evdref env assums arity indname =
   (is_ml_type,indname,assums)
 
 let prepare_param = function
-  | LocalAssum (na,t) -> out_name na, LocalAssumEntry t
-  | LocalDef (na,b,_) -> out_name na, LocalDefEntry b
+  | LocalAssum (na,t) -> Name.get_id na, LocalAssumEntry t
+  | LocalDef (na,b,_) -> Name.get_id na, LocalDefEntry b
 
 (** Make the arity conclusion flexible to avoid generating an upper bound universe now,
     only if the universe does not appear anywhere else.
@@ -590,7 +590,7 @@ let interp_mutual_inductive (paramsl,indl) notations poly prv finite =
       
   (* Names of parameters as arguments of the inductive type (defs removed) *)
   let assums = List.filter is_local_assum ctx_params in
-  let params = List.map (RelDecl.get_name %> out_name) assums in
+  let params = List.map (RelDecl.get_name %> Name.get_id) assums in
 
   (* Interpret the arities *)
   let arities = List.map (interp_ind_arity env_params evdref) indl in
diff --git a/vernac/himsg.ml b/vernac/himsg.ml
index 17bb87f2aa..6d8dd82ac6 100644
--- a/vernac/himsg.ml
+++ b/vernac/himsg.ml
@@ -682,12 +682,12 @@ let explain_wrong_abstraction_type env sigma na abs expected result =
 
 let explain_abstraction_over_meta _ m n =
   strbrk "Too complex unification problem: cannot find a solution for both " ++
-  pr_name m ++ spc () ++ str "and " ++ pr_name n ++ str "."
+  Name.print m ++ spc () ++ str "and " ++ Name.print n ++ str "."
 
 let explain_non_linear_unification env sigma m t =
   let t = EConstr.to_constr sigma t in
   strbrk "Cannot unambiguously instantiate " ++
-  pr_name m ++ str ":" ++
+  Name.print m ++ str ":" ++
   strbrk " which would require to abstract twice on " ++
   pr_lconstr_env env sigma t ++ str "."
 
@@ -1055,7 +1055,7 @@ let explain_refiner_bad_type arg ty conclty =
 let explain_refiner_unresolved_bindings l =
   str "Unable to find an instance for the " ++
   str (String.plural (List.length l) "variable") ++ spc () ++
-  prlist_with_sep pr_comma pr_name l ++ str"."
+  prlist_with_sep pr_comma Name.print l ++ str"."
 
 let explain_refiner_cannot_apply t harg =
   str "In refiner, a term of type" ++ brk(1,1) ++
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 6c1d64cfe9..405d37927f 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -1003,12 +1003,12 @@ let vernac_arguments locality reference args more_implicits nargs_for_red flags
   let err_extra_args names =
     user_err ~hdr:"vernac_declare_arguments"
                  (strbrk "Extra arguments: " ++
-                    prlist_with_sep pr_comma pr_name names ++ str ".")
+                    prlist_with_sep pr_comma Name.print names ++ str ".")
   in
   let err_missing_args names =
     user_err ~hdr:"vernac_declare_arguments"
                  (strbrk "The following arguments are not declared: " ++
-                    prlist_with_sep pr_comma pr_name names ++ str ".")
+                    prlist_with_sep pr_comma Name.print names ++ str ".")
   in
 
   let rec check_extra_args extra_args =
@@ -1093,14 +1093,14 @@ let vernac_arguments locality reference args more_implicits nargs_for_red flags
        match !example_renaming with
        | None -> mt ()
        | Some (o,n) ->
-          str "Argument " ++ pr_name o ++
-            str " renamed to " ++ pr_name n ++ str ".");
+          str "Argument " ++ Name.print o ++
+            str " renamed to " ++ Name.print n ++ str ".");
 
   let duplicate_names =
     List.duplicates Name.equal (List.filter ((!=) Anonymous) names)
   in
   if not (List.is_empty duplicate_names) then begin
-    let duplicates = prlist_with_sep pr_comma pr_name duplicate_names in
+    let duplicates = prlist_with_sep pr_comma Name.print duplicate_names in
     user_err (strbrk "Some argument names are duplicated: " ++ duplicates)
   end;
 
@@ -1129,7 +1129,7 @@ let vernac_arguments locality reference args more_implicits nargs_for_red flags
        anonymous argument implicit *)
     | Anonymous :: _, (name, _) :: _ ->
        user_err ~hdr:"vernac_declare_arguments"
-                    (strbrk"Argument "++ pr_name name ++ 
+                    (strbrk"Argument "++ Name.print name ++ 
                        strbrk " cannot be declared implicit.")
 
     | Name id :: inf_names, (name, impl) :: implicits ->