4 files changed, 3 insertions, 19 deletions
diff --git a/kernel/univ.ml b/kernel/univ.ml
index 256ce5e92c..08a7e94544 100644
--- a/kernel/univ.ml
+++ b/kernel/univ.ml
@@ -1708,7 +1708,6 @@ module Instance : sig
 
     val eqeq : t -> t -> bool
     val subst_fn : universe_level_subst_fn -> t -> t
-    val subst : universe_level_subst -> t -> t
     
     val pr : t -> Pp.std_ppcmds
     val levels : t -> LSet.t
@@ -1763,7 +1762,7 @@ struct
     
   let hash = HInstancestruct.hash
     
-  let share a = (a, hash a)
+  let share a = (hcons a, hash a)
 	      
   let empty = hcons [||]
 
@@ -1782,12 +1781,7 @@ struct
 
   let subst_fn fn t = 
     let t' = CArray.smartmap fn t in
-      if t' == t then t else hcons t'
-
-  let subst s t =
-    let t' = 
-      CArray.smartmap (fun x -> try LMap.find x s with Not_found -> x) t
-    in if t' == t then t else hcons t'
+      if t' == t then t else t'
 
   let levels x = LSet.of_array x
 
diff --git a/kernel/univ.mli b/kernel/univ.mli
index 9b68dbc8ce..25d25fa353 100644
--- a/kernel/univ.mli
+++ b/kernel/univ.mli
@@ -272,7 +272,7 @@ sig
   (** To concatenate two instances, used for discharge *)
 
   val equal : t -> t -> bool
-  (** Equality (note: instances are hash-consed, this is O(1)) *)
+  (** Equality *)
 
   val hcons : t -> t
   (** Hash-consing. *)
@@ -289,9 +289,6 @@ sig
   val subst_fn : universe_level_subst_fn -> t -> t
   (** Substitution by a level-to-level function. *)
 
-  val subst : universe_level_subst -> t -> t
-  (** Substitution by a level-to-level function. *)
-
   val pr : t -> Pp.std_ppcmds
   (** Pretty-printing, no comments *)
 
diff --git a/kernel/vars.ml b/kernel/vars.ml
index 120c07d30d..386a3e8ff2 100644
--- a/kernel/vars.ml
+++ b/kernel/vars.ml
@@ -216,12 +216,6 @@ let subst_vars subst c = substn_vars 1 subst c
 (** Universe substitutions *)
 open Constr
 
-let subst_univs_puniverses subst =
-  if Univ.is_empty_level_subst subst then fun c -> c
-  else 
-    let f = Univ.Instance.subst subst in
-      fun ((c, u) as x) -> let u' = f u in if u' == u then x else (c, u')
-
 let subst_univs_fn_puniverses fn =
   let f = Univ.Instance.subst_fn fn in
     fun ((c, u) as x) -> let u' = f u in if u' == u then x else (c, u')
diff --git a/kernel/vars.mli b/kernel/vars.mli
index b4f616b139..0d5ab07db0 100644
--- a/kernel/vars.mli
+++ b/kernel/vars.mli
@@ -81,6 +81,5 @@ val subst_univs_constr : universe_subst -> constr -> constr
 
 (** Level substitutions for polymorphism. *)
 
-val subst_univs_puniverses : universe_level_subst -> 'a puniverses -> 'a puniverses
 val subst_univs_level_constr : universe_level_subst -> constr -> constr
 val subst_univs_level_context : Univ.universe_level_subst -> rel_context -> rel_context