diff options
Diffstat (limited to 'kernel')
| -rw-r--r-- | kernel/constr.ml | 2 | ||||
| -rw-r--r-- | kernel/names.ml | 20 | ||||
| -rw-r--r-- | kernel/sorts.ml | 2 | ||||
| -rw-r--r-- | kernel/univ.ml | 10 |
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) |