Ensuring the good invariants of hashcons table generation in the API.

4 files changed, 17 insertions, 17 deletions

diff --git a/kernel/constr.ml b/kernel/constr.ml
index e757c5b560..a01a534eea 100644
--- a/kernel/constr.ml
+++ b/kernel/constr.ml
@@ -991,7 +991,7 @@ module Hsorts =
     end)
 
 (* let hcons_sorts = Hashcons.simple_hcons Hsorts.generate hcons_univ *)
-let hcons_caseinfo = Hashcons.simple_hcons Hcaseinfo.generate hcons_ind
+let hcons_caseinfo = Hashcons.simple_hcons Hcaseinfo.generate Hcaseinfo.hcons hcons_ind
 
 let hcons =
   hashcons
diff --git a/kernel/names.ml b/kernel/names.ml
index 13ea9e1d86..181f6c45ea 100644
--- a/kernel/names.ml
+++ b/kernel/names.ml
@@ -108,7 +108,7 @@ struct
 
   module Hname = Hashcons.Make(Self_Hashcons)
 
-  let hcons = Hashcons.simple_hcons Hname.generate Id.hcons
+  let hcons = Hashcons.simple_hcons Hname.generate Hname.hcons Id.hcons
 
 end
 
@@ -175,7 +175,7 @@ struct
 
   module Hdir = Hashcons.Hlist(Id)
 
-  let hcons = Hashcons.recursive_hcons Hdir.generate Id.hcons
+  let hcons = Hashcons.recursive_hcons Hdir.generate Hdir.hcons Id.hcons
 
 end
 
@@ -239,7 +239,7 @@ struct
 
   module HashMBId = Hashcons.Make(Self_Hashcons)
 
-  let hcons = Hashcons.simple_hcons HashMBId.generate (Id.hcons, DirPath.hcons)
+  let hcons = Hashcons.simple_hcons HashMBId.generate HashMBId.hcons (Id.hcons, DirPath.hcons)
 
 end
 
@@ -335,7 +335,7 @@ module ModPath = struct
   module HashMP = Hashcons.Make(Self_Hashcons)
 
   let hcons =
-    Hashcons.simple_hcons HashMP.generate
+    Hashcons.simple_hcons HashMP.generate HashMP.hcons
       (DirPath.hcons,MBId.hcons,String.hcons)
 
 end
@@ -427,7 +427,7 @@ module KerName = struct
   module HashKN = Hashcons.Make(Self_Hashcons)
 
   let hcons =
-    Hashcons.simple_hcons HashKN.generate
+    Hashcons.simple_hcons HashKN.generate HashKN.hcons
       (ModPath.hcons,DirPath.hcons,String.hcons)
 end
 
@@ -663,10 +663,10 @@ module Hconstruct = Hashcons.Make(
     let hash = constructor_hash
   end)
 
-let hcons_con = Hashcons.simple_hcons Constant.HashKP.generate KerName.hcons
-let hcons_mind = Hashcons.simple_hcons MutInd.HashKP.generate KerName.hcons
-let hcons_ind = Hashcons.simple_hcons Hind.generate hcons_mind
-let hcons_construct = Hashcons.simple_hcons Hconstruct.generate hcons_ind
+let hcons_con = Hashcons.simple_hcons Constant.HashKP.generate Constant.HashKP.hcons KerName.hcons
+let hcons_mind = Hashcons.simple_hcons MutInd.HashKP.generate MutInd.HashKP.hcons KerName.hcons
+let hcons_ind = Hashcons.simple_hcons Hind.generate Hind.hcons hcons_mind
+let hcons_construct = Hashcons.simple_hcons Hconstruct.generate Hconstruct.hcons hcons_ind
 
 (*****************)
 
@@ -810,7 +810,7 @@ struct
 
   module HashProjection = Hashcons.Make(Self_Hashcons)
 
-  let hcons = Hashcons.simple_hcons HashProjection.generate hcons_con
+  let hcons = Hashcons.simple_hcons HashProjection.generate HashProjection.hcons hcons_con
 
   let compare (c, b) (c', b') =
     if b == b' then Constant.CanOrd.compare c c'
diff --git a/kernel/sorts.ml b/kernel/sorts.ml
index bfcdc0b4df..1462aad910 100644
--- a/kernel/sorts.ml
+++ b/kernel/sorts.ml
@@ -104,4 +104,4 @@ module Hsorts =
       let hash = Hashtbl.hash (** FIXME *)
     end)
 
-let hcons = Hashcons.simple_hcons Hsorts.generate hcons_univ
+let hcons = Hashcons.simple_hcons Hsorts.generate Hsorts.hcons hcons_univ
diff --git a/kernel/univ.ml b/kernel/univ.ml
index dd43e17be5..2cac50fda7 100644
--- a/kernel/univ.ml
+++ b/kernel/univ.ml
@@ -488,7 +488,7 @@ struct
       include Hashcons.Make(ExprHash)
 
       let make =
-	Hashcons.simple_hcons generate Level.hcons
+	Hashcons.simple_hcons generate hcons Level.hcons
       let hash = ExprHash.hash
       let equal x y = x == y ||
 	(let (u,n) = x and (v,n') = y in
@@ -1391,8 +1391,8 @@ module Hconstraints =
       let hash = Hashtbl.hash
     end)
 
-let hcons_constraint = Hashcons.simple_hcons Hconstraint.generate Level.hcons
-let hcons_constraints = Hashcons.simple_hcons Hconstraints.generate hcons_constraint
+let hcons_constraint = Hashcons.simple_hcons Hconstraint.generate Hconstraint.hcons Level.hcons
+let hcons_constraints = Hashcons.simple_hcons Hconstraints.generate Hconstraints.hcons hcons_constraint
 
 
 (** A value with universe constraints. *)
@@ -1775,7 +1775,7 @@ struct
 
   module HInstance = Hashcons.Make(HInstancestruct)
 
-  let hcons = Hashcons.simple_hcons HInstance.generate Level.hcons
+  let hcons = Hashcons.simple_hcons HInstance.generate HInstance.hcons Level.hcons
     
   let hash = HInstancestruct.hash
     
@@ -2125,7 +2125,7 @@ module Huniverse_set =
     end)
 
 let hcons_universe_set = 
-  Hashcons.simple_hcons Huniverse_set.generate Level.hcons
+  Hashcons.simple_hcons Huniverse_set.generate Huniverse_set.hcons Level.hcons
 
 let hcons_universe_context_set (v, c) = 
   (hcons_universe_set v, hcons_constraints c)