Cleaning, renaming obscure functions and documenting in Hashcons.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15834 85f007b7-540e-0410-9357-904b9bb8a0f7

3 files changed, 33 insertions, 33 deletions

diff --git a/kernel/names.ml b/kernel/names.ml
index 6146e10839..d2c06104be 100644
--- a/kernel/names.ml
+++ b/kernel/names.ml
@@ -353,7 +353,7 @@ module Hname = Hashcons.Make(
   struct
     type t = name
     type u = identifier -> identifier
-    let hash_sub hident = function
+    let hashcons hident = function
       | Name id -> Name (hident id)
       | n -> n
     let equal n1 n2 =
@@ -369,7 +369,7 @@ module Hdir = Hashcons.Make(
   struct
     type t = dir_path
     type u = identifier -> identifier
-    let hash_sub hident d = List.smartmap hident d
+    let hashcons hident d = List.smartmap hident d
     let rec equal d1 d2 =
       (d1==d2) ||
       match (d1,d2) with
@@ -383,7 +383,7 @@ module Huniqid = Hashcons.Make(
   struct
     type t = uniq_ident
     type u = (identifier -> identifier) * (dir_path -> dir_path)
-    let hash_sub (hid,hdir) (n,s,dir) = (n,hid s,hdir dir)
+    let hashcons (hid,hdir) (n,s,dir) = (n,hid s,hdir dir)
     let equal ((n1,s1,dir1) as x) ((n2,s2,dir2) as y) =
       (x == y) ||
       (n1 = n2 && s1 == s2 && dir1 == dir2)
@@ -395,10 +395,10 @@ module Hmod = Hashcons.Make(
     type t = module_path
     type u = (dir_path -> dir_path) * (uniq_ident -> uniq_ident) *
 	(string -> string)
-    let rec hash_sub (hdir,huniqid,hstr as hfuns) = function
+    let rec hashcons (hdir,huniqid,hstr as hfuns) = function
       | MPfile dir -> MPfile (hdir dir)
       | MPbound m -> MPbound (huniqid m)
-      | MPdot (md,l) -> MPdot (hash_sub hfuns md, hstr l)
+      | MPdot (md,l) -> MPdot (hashcons hfuns md, hstr l)
     let rec equal d1 d2 =
       d1 == d2 ||
       match (d1,d2) with
@@ -414,7 +414,7 @@ module Hkn = Hashcons.Make(
     type t = kernel_name
     type u = (module_path -> module_path)
 	* (dir_path -> dir_path) * (string -> string)
-    let hash_sub (hmod,hdir,hstr) (md,dir,l) =
+    let hashcons (hmod,hdir,hstr) (md,dir,l) =
       (hmod md, hdir dir, hstr l)
     let equal (mod1,dir1,l1) (mod2,dir2,l2) =
       mod1 == mod2 && dir1 == dir2 && l1 == l2
@@ -429,7 +429,7 @@ module Hcn = Hashcons.Make(
   struct
     type t = kernel_name*kernel_name
     type u = kernel_name -> kernel_name
-    let hash_sub hkn (user,can) = (hkn user, hkn can)
+    let hashcons hkn (user,can) = (hkn user, hkn can)
     let equal (user1,_) (user2,_) = user1 == user2
     let hash (user,_) = Hashtbl.hash user
   end)
@@ -438,7 +438,7 @@ module Hind = Hashcons.Make(
   struct
     type t = inductive
     type u = mutual_inductive -> mutual_inductive
-    let hash_sub hmind (mind, i) = (hmind mind, i)
+    let hashcons hmind (mind, i) = (hmind mind, i)
     let equal (mind1,i1) (mind2,i2) = mind1 == mind2 && i1 = i2
     let hash = Hashtbl.hash
   end)
@@ -447,23 +447,23 @@ module Hconstruct = Hashcons.Make(
   struct
     type t = constructor
     type u = inductive -> inductive
-    let hash_sub hind (ind, j) = (hind ind, j)
+    let hashcons hind (ind, j) = (hind ind, j)
     let equal (ind1,j1) (ind2,j2) = ind1 == ind2 && j1 = j2
     let hash = Hashtbl.hash
   end)
 
-let hcons_string = Hashcons.simple_hcons Hashcons.Hstring.f ()
+let hcons_string = Hashcons.simple_hcons Hashcons.Hstring.generate ()
 let hcons_ident = hcons_string
-let hcons_name = Hashcons.simple_hcons Hname.f hcons_ident
-let hcons_dirpath = Hashcons.simple_hcons Hdir.f hcons_ident
-let hcons_uid = Hashcons.simple_hcons Huniqid.f (hcons_ident,hcons_dirpath)
+let hcons_name = Hashcons.simple_hcons Hname.generate hcons_ident
+let hcons_dirpath = Hashcons.simple_hcons Hdir.generate hcons_ident
+let hcons_uid = Hashcons.simple_hcons Huniqid.generate (hcons_ident,hcons_dirpath)
 let hcons_mp =
-  Hashcons.simple_hcons Hmod.f (hcons_dirpath,hcons_uid,hcons_string)
-let hcons_kn = Hashcons.simple_hcons Hkn.f (hcons_mp,hcons_dirpath,hcons_string)
-let hcons_con = Hashcons.simple_hcons Hcn.f hcons_kn
-let hcons_mind = Hashcons.simple_hcons Hcn.f hcons_kn
-let hcons_ind = Hashcons.simple_hcons Hind.f hcons_mind
-let hcons_construct = Hashcons.simple_hcons Hconstruct.f hcons_ind
+  Hashcons.simple_hcons Hmod.generate (hcons_dirpath,hcons_uid,hcons_string)
+let hcons_kn = Hashcons.simple_hcons Hkn.generate (hcons_mp,hcons_dirpath,hcons_string)
+let hcons_con = Hashcons.simple_hcons Hcn.generate hcons_kn
+let hcons_mind = Hashcons.simple_hcons Hcn.generate hcons_kn
+let hcons_ind = Hashcons.simple_hcons Hind.generate hcons_mind
+let hcons_construct = Hashcons.simple_hcons Hconstruct.generate hcons_ind
 
 
 (*******)
diff --git a/kernel/term.ml b/kernel/term.ml
index e54e56f12f..8ab04af24e 100644
--- a/kernel/term.ml
+++ b/kernel/term.ml
@@ -1236,9 +1236,9 @@ let equals_constr t1 t2 =
 (** Note that the following Make has the side effect of creating
     once and for all the table we'll use for hash-consing all constr *)
 
-module H = Hashtbl_alt.Make(struct type t = constr let equals = equals_constr end)
+module H = Hashset.Make(struct type t = constr let equal = equals_constr end)
 
-open Hashtbl_alt.Combine
+open Hashset.Combine
 
 (* [hcons_term hash_consing_functions constr] computes an hash-consed
    representation for [constr] using [hash_consing_functions] on
@@ -1369,7 +1369,7 @@ module Hsorts =
     struct
       type t = sorts
       type u = universe -> universe
-      let hash_sub huniv = function
+      let hashcons huniv = function
           Prop c -> Prop c
         | Type u -> Type (huniv u)
       let equal s1 s2 =
@@ -1385,7 +1385,7 @@ module Hcaseinfo =
     struct
       type t = case_info
       type u = inductive -> inductive
-      let hash_sub hind ci = { ci with ci_ind = hind ci.ci_ind }
+      let hashcons hind ci = { ci with ci_ind = hind ci.ci_ind }
       let equal ci ci' =
 	ci.ci_ind == ci'.ci_ind &&
 	ci.ci_npar = ci'.ci_npar &&
@@ -1394,8 +1394,8 @@ module Hcaseinfo =
       let hash = Hashtbl.hash
     end)
 
-let hcons_sorts = Hashcons.simple_hcons Hsorts.f hcons_univ
-let hcons_caseinfo = Hashcons.simple_hcons Hcaseinfo.f hcons_ind
+let hcons_sorts = Hashcons.simple_hcons Hsorts.generate hcons_univ
+let hcons_caseinfo = Hashcons.simple_hcons Hcaseinfo.generate hcons_ind
 
 let hcons_constr =
   hcons_term
diff --git a/kernel/univ.ml b/kernel/univ.ml
index 9334a06d13..faadb10818 100644
--- a/kernel/univ.ml
+++ b/kernel/univ.ml
@@ -874,7 +874,7 @@ module Hunivlevel =
     struct
       type t = universe_level
       type u = Names.dir_path -> Names.dir_path
-      let hash_sub hdir = function
+      let hashcons hdir = function
 	| UniverseLevel.Set -> UniverseLevel.Set
 	| UniverseLevel.Level (n,d) -> UniverseLevel.Level (n,hdir d)
       let equal l1 l2 =
@@ -892,7 +892,7 @@ module Huniv =
     struct
       type t = universe
       type u = universe_level -> universe_level
-      let hash_sub hdir = function
+      let hashcons hdir = function
 	| Atom u -> Atom (hdir u)
 	| Max (gel,gtl) -> Max (List.map hdir gel, List.map hdir gtl)
       let equal u v =
@@ -906,15 +906,15 @@ module Huniv =
       let hash = Hashtbl.hash
     end)
 
-let hcons_univlevel = Hashcons.simple_hcons Hunivlevel.f Names.hcons_dirpath
-let hcons_univ = Hashcons.simple_hcons Huniv.f hcons_univlevel
+let hcons_univlevel = Hashcons.simple_hcons Hunivlevel.generate Names.hcons_dirpath
+let hcons_univ = Hashcons.simple_hcons Huniv.generate hcons_univlevel
 
 module Hconstraint =
   Hashcons.Make(
     struct
       type t = univ_constraint
       type u = universe_level -> universe_level
-      let hash_sub hul (l1,k,l2) = (hul l1, k, hul l2)
+      let hashcons hul (l1,k,l2) = (hul l1, k, hul l2)
       let equal (l1,k,l2) (l1',k',l2') =
 	l1 == l1' && k = k' && l2 == l2'
       let hash = Hashtbl.hash
@@ -925,7 +925,7 @@ module Hconstraints =
     struct
       type t = constraints
       type u = univ_constraint -> univ_constraint
-      let hash_sub huc s =
+      let hashcons huc s =
 	Constraint.fold (fun x -> Constraint.add (huc x)) s Constraint.empty
       let equal s s' =
 	List.for_all2eq (==)
@@ -934,5 +934,5 @@ module Hconstraints =
       let hash = Hashtbl.hash
     end)
 
-let hcons_constraint = Hashcons.simple_hcons Hconstraint.f hcons_univlevel
-let hcons_constraints = Hashcons.simple_hcons Hconstraints.f hcons_constraint
+let hcons_constraint = Hashcons.simple_hcons Hconstraint.generate hcons_univlevel
+let hcons_constraints = Hashcons.simple_hcons Hconstraints.generate hcons_constraint