Remove specific hash-consing of Term.types (was unused anyway)

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

2 files changed, 4 insertions, 32 deletions

diff --git a/kernel/term.ml b/kernel/term.ml
index 4c6c8e3388..1ed9185190 100644
--- a/kernel/term.ml
+++ b/kernel/term.ml
@@ -1367,22 +1367,6 @@ let rec hash_constr t =
 and hash_term_array t =
   Array.fold_left (fun acc t -> combine (hash_constr t) acc) 0 t
 
-module Htype =
-  Hashcons.Make(
-    struct
-      type t = types
-      type u = (constr -> constr) * (sorts -> sorts)
-(*
-      let hash_sub (hc,hs) j = {body=hc j.body; typ=hs j.typ}
-      let equal j1 j2 = j1.body==j2.body & j1.typ==j2.typ
-*)
-(**)
-      let hash_sub (hc,hs) j = hc j
-      let equal j1 j2 = j1==j2
-(**)
-      let hash = Hashtbl.hash
-    end)
-
 module Hsorts =
   Hashcons.Make(
     struct
@@ -1401,14 +1385,12 @@ module Hsorts =
 
 let hsort = Hsorts.f
 
-let hcons_constr (hcon,hkn,hdir,hname,hident) =
+let hcons1_constr =
+  let (hcon,hkn,hdir,hname,hident) = hcons_names in
   let hsortscci = Hashcons.simple_hcons hsort hcons1_univ in
-  let hcci = hcons_term (hsortscci,hcon,hkn,hname,hident) in
-  let htcci = Hashcons.simple_hcons Htype.f (hcci,hsortscci) in
-  (hcci,htcci)
-
-let (hcons1_constr, hcons1_types) = hcons_constr hcons_names
+  hcons_term (hsortscci,hcon,hkn,hname,hident)
 
+let hcons1_types = hcons1_constr
 
 (*******)
 (* Type of abstract machine values *)
diff --git a/kernel/term.mli b/kernel/term.mli
index aa9a55abc0..2ec1bd9b96 100644
--- a/kernel/term.mli
+++ b/kernel/term.mli
@@ -626,16 +626,6 @@ val hash_constr : constr -> int
 
 (*********************************************************************)
 
-val hcons_constr:
-  (constant -> constant) *
-  (mutual_inductive -> mutual_inductive) *
-  (dir_path -> dir_path) *
-  (name -> name) *
-  (identifier -> identifier)
-  ->
-    (constr -> constr) *
-    (types -> types)
-
 val hcons1_constr : constr -> constr
 val hcons1_types : types -> types