From 8ab00e5f272aa8f16d70a00323c57f2d4ef66f03 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Thu, 13 Apr 2017 21:41:41 +0200
Subject: 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.
---
 plugins/ltac/pptactic.ml   | 2 +-
 plugins/ltac/tacentries.ml | 2 +-
 plugins/ltac/tacintern.ml  | 2 +-
 plugins/ltac/tacinterp.ml  | 6 +++---
 4 files changed, 6 insertions(+), 6 deletions(-)

(limited to 'plugins/ltac')

diff --git a/plugins/ltac/pptactic.ml b/plugins/ltac/pptactic.ml
index a001c6a2ba..67d2b452ac 100644
--- a/plugins/ltac/pptactic.ml
+++ b/plugins/ltac/pptactic.ml
@@ -571,7 +571,7 @@ type 'a extra_genarg_printer =
               str "=>" ++ brk (1,4) ++ pr t))
     | All t -> str "_" ++ spc () ++ str "=>" ++ brk (1,4) ++ pr t
 
-  let pr_funvar n = spc () ++ pr_name n
+  let pr_funvar n = spc () ++ Name.print n
 
   let pr_let_clause k pr (id,(bl,t)) =
     hov 0 (keyword k ++ spc () ++ pr_lident id ++ prlist pr_funvar bl ++
diff --git a/plugins/ltac/tacentries.ml b/plugins/ltac/tacentries.ml
index 75f89a81e1..f44ccbd3b5 100644
--- a/plugins/ltac/tacentries.ml
+++ b/plugins/ltac/tacentries.ml
@@ -502,7 +502,7 @@ let print_ltacs () =
     | Tacexpr.TacFun (l, t) -> (l, t)
     | _ -> ([], body)
     in
-    let pr_ltac_fun_arg n = spc () ++ pr_name n in
+    let pr_ltac_fun_arg n = spc () ++ Name.print n in
     hov 2 (pr_qualid qid ++ prlist pr_ltac_fun_arg l)
   in
   Feedback.msg_notice (prlist_with_sep fnl pr_entry entries)
diff --git a/plugins/ltac/tacintern.ml b/plugins/ltac/tacintern.ml
index e431a13bc2..82711dd46a 100644
--- a/plugins/ltac/tacintern.ml
+++ b/plugins/ltac/tacintern.ml
@@ -718,7 +718,7 @@ let split_ltac_fun = function
   | TacFun (l,t) -> (l,t)
   | t -> ([],t)
 
-let pr_ltac_fun_arg n = spc () ++ pr_name n
+let pr_ltac_fun_arg n = spc () ++ Name.print n
 
 let print_ltac id =
  try
diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml
index a9ec779d11..31c1b79ee0 100644
--- a/plugins/ltac/tacinterp.ml
+++ b/plugins/ltac/tacinterp.ml
@@ -1116,11 +1116,11 @@ let cons_and_check_name id l =
 
 let rec read_match_goal_hyps lfun ist env sigma lidh = function
   | (Hyp ((loc,na) as locna,mp))::tl ->
-      let lidh' = name_fold cons_and_check_name na lidh in
+      let lidh' = Name.fold_right cons_and_check_name na lidh in
       Hyp (locna,read_pattern lfun ist env sigma mp)::
 	(read_match_goal_hyps lfun ist env sigma lidh' tl)
   | (Def ((loc,na) as locna,mv,mp))::tl ->
-      let lidh' = name_fold cons_and_check_name na lidh in
+      let lidh' = Name.fold_right cons_and_check_name na lidh in
       Def (locna,read_pattern lfun ist env sigma mv, read_pattern lfun ist env sigma mp)::
 	(read_match_goal_hyps lfun ist env sigma lidh' tl)
   | [] -> []
@@ -1423,7 +1423,7 @@ and tactic_of_value ist vle =
       (str "A fully applied tactic is expected:" ++ spc() ++ Pp.str "missing " ++
        Pp.str (String.plural numargs "argument") ++ Pp.str " for " ++
        Pp.str (String.plural numargs "variable") ++ Pp.str " " ++
-       pr_enum pr_name vars ++ Pp.str ".")
+       pr_enum Name.print vars ++ Pp.str ".")
   | VRec _ -> Tacticals.New.tclZEROMSG (str "A fully applied tactic is expected.")
   else if has_type vle (topwit wit_tactic) then
     let tac = out_gen (topwit wit_tactic) vle in
-- 
cgit v1.2.3