diff options
Diffstat (limited to 'engine/nameops.ml')
| -rw-r--r-- | engine/nameops.ml | 28 |
1 files changed, 1 insertions, 27 deletions
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 - |