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.

1 files changed, 3 insertions, 3 deletions

diff --git a/vernac/himsg.ml b/vernac/himsg.ml
index 17bb87f2a..6d8dd82ac 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) ++