From 9ebf44d84754adc5b64fcf612c6816c02c80462d Mon Sep 17 00:00:00 2001
From: Benjamin Barenblat <bbaren@debian.org>
Date: Sat, 2 Feb 2019 19:29:23 -0500
Subject: Imported Upstream version 8.9.0

---
 engine/nameops.ml | 28 +---------------------------
 1 file changed, 1 insertion(+), 27 deletions(-)

(limited to 'engine/nameops.ml')

diff --git a/engine/nameops.ml b/engine/nameops.ml
index 53969caf..15e20134 100644
--- a/engine/nameops.ml
+++ b/engine/nameops.ml
@@ -11,10 +11,6 @@
 open Util
 open Names
 
-(* Identifiers *)
-
-let pr_id id = Id.print id
-
 (* Utilities *)
 
 let code_of_0 = Char.code '0'
@@ -73,7 +69,7 @@ let root_of_id id =
    [bar0]  ↦ [bar1]
    [bar00] ↦ [bar01]
    [bar1]  ↦ [bar2]
-   [bar01] ↦ [bar01]
+   [bar01] ↦ [bar02]
    [bar9]  ↦ [bar10]
    [bar09] ↦ [bar10]
    [bar99] ↦ [bar100]
@@ -191,28 +187,6 @@ struct
 
 end
 
-open Name
-
-(* Compatibility *)
-let out_name = get_id
-let name_fold = fold_right
-let name_iter = iter
-let name_app = map
-let name_fold_map = fold_left_map
-let name_cons = cons
-let name_max = pick
-let pr_name = print
-
-let pr_lab l = Label.print l
-
 (* Metavariables *)
 let pr_meta = Pp.int
 let string_of_meta = string_of_int
-
-(* Deprecated *)
-open Libnames
-let default_library = default_library
-let coq_string = coq_string
-let coq_root = coq_root
-let default_root_prefix = default_root_prefix
-
-- 
cgit v1.2.3