1 files changed, 29 insertions, 36 deletions

diff --git a/kernel/names.ml b/kernel/names.ml
index 1eb9a31751..d7c0a5e980 100644
--- a/kernel/names.ml
+++ b/kernel/names.ml
@@ -34,33 +34,28 @@ struct
 
   let hash = String.hash
 
-  let warn_invalid_identifier =
-    CWarnings.create ~name:"invalid-identifier" ~category:"parsing"
-                     ~default:CWarnings.Disabled
-                     (fun s -> str s)
-
-  let check_soft ?(warn = true) x =
-    let iter (fatal, x) =
-      if fatal then CErrors.error x else
-        if warn then warn_invalid_identifier x
-    in
+  let check_valid ?(strict=true) x =
+    let iter (fatal, x) = if fatal || strict then CErrors.user_err Pp.(str x) in
     Option.iter iter (Unicode.ident_refutation x)
 
   let is_valid s = match Unicode.ident_refutation s with
   | None -> true
   | Some _ -> false
 
+  let of_bytes s =
+    let s = Bytes.to_string s in
+    check_valid s;
+    String.hcons s
+
   let of_string s =
-    let () = check_soft s in
-    let s = String.copy s in
+    let () = check_valid s in
     String.hcons s
 
   let of_string_soft s =
-    let () = check_soft ~warn:false s in
-    let s = String.copy s in
+    let () = check_valid ~strict:false s in
     String.hcons s
 
-  let to_string id = String.copy id
+  let to_string id = id
 
   let print id = str id
 
@@ -88,11 +83,14 @@ struct
   type t = Anonymous     (** anonymous identifier *)
 	 | Name of Id.t  (** non-anonymous identifier *)
 
+  let mk_name id =
+    Name id
+
   let is_anonymous = function
     | Anonymous -> true
     | Name _ -> false
 
-  let is_name = not % is_anonymous
+  let is_name = is_anonymous %> not
 
   let compare n1 n2 = match n1, n2 with
     | Anonymous, Anonymous -> 0
@@ -106,8 +104,12 @@ struct
     | _ -> false
 
   let hash = function
-  | Anonymous -> 0
-  | Name id -> Id.hash id
+    | Anonymous -> 0
+    | Name id -> Id.hash id
+
+  let print = function
+    | Anonymous -> str "_"
+    | Name id -> Id.print id
 
   module Self_Hashcons =
     struct
@@ -156,21 +158,8 @@ module DirPath =
 struct
   type t = module_ident list
 
-  let rec compare (p1 : t) (p2 : t) =
-    if p1 == p2 then 0
-    else begin match p1, p2 with
-    | [], [] -> 0
-    | [], _ -> -1
-    | _, [] -> 1
-    | id1 :: p1, id2 :: p2 ->
-      let c = Id.compare id1 id2 in
-      if Int.equal c 0 then compare p1 p2 else c
-    end
-
-  let rec equal p1 p2 = p1 == p2 || match p1, p2 with
-  | [], [] -> true
-  | id1 :: p1, id2 :: p2 -> Id.equal id1 id2 && equal p1 p2
-  | _ -> false
+  let compare = List.compare Id.compare
+  let equal = List.equal Id.equal
 
   let rec hash accu = function
   | [] -> accu
@@ -185,7 +174,7 @@ struct
 
   let empty = []
 
-  let is_empty d = match d with [] -> true | _ -> false
+  let is_empty = List.is_empty
 
   let to_string = function
     | [] -> "<>"
@@ -549,7 +538,6 @@ module KerPair = struct
   end
 
   module SyntacticOrd = struct
-    type t = kernel_pair
     let compare x y = match x, y with
       | Same knx, Same kny -> KerName.compare knx kny
       | Dual (knux,kncx), Dual (knuy,kncy) ->
@@ -601,7 +589,13 @@ end
 module Constant = KerPair
 
 module Cmap = HMap.Make(Constant.CanOrd)
+(** A map whose keys are constants (values of the {!Constant.t} type).
+    Keys are ordered wrt. "canonical form" of the constant. *)
+
 module Cmap_env = HMap.Make(Constant.UserOrd)
+(** A map whose keys are constants (values of the {!Constant.t} type).
+    Keys are ordered wrt. "user form" of the constant. *)
+
 module Cpred = Predicate.Make(Constant.CanOrd)
 module Cset = Cmap.Set
 module Cset_env = Cmap_env.Set
@@ -866,7 +860,6 @@ struct
   let hash (c, b) = (if b then 0 else 1) + Constant.hash c
 
   module SyntacticOrd = struct
-    type t = constant * bool
     let compare (c, b) (c', b') =
       if b = b' then Constant.SyntacticOrd.compare c c' else -1
     let equal (c, b as x) (c', b' as x') =