5 files changed, 0 insertions, 38 deletions
diff --git a/engine/uState.ml b/engine/uState.ml
index 20ea24dd87..81559778f2 100644
--- a/engine/uState.ml
+++ b/engine/uState.ml
@@ -296,9 +296,6 @@ let add_constraints uctx cstrs =
     universes = UGraph.merge_constraints cstrs' uctx.universes;
     weak_constraints = weak; }
 
-(* let addconstrkey = CProfile.declare_profile "add_constraints_context";; *)
-(* let add_constraints_context = CProfile.profile2 addconstrkey add_constraints_context;; *)
-
 let add_universe_constraints uctx cstrs =
   let univs, local = uctx.local in
   let vars, weak, local' = process_universe_constraints uctx cstrs in
diff --git a/engine/univMinim.ml b/engine/univMinim.ml
index 4ed6e97526..86bf2c9298 100644
--- a/engine/univMinim.ml
+++ b/engine/univMinim.ml
@@ -406,6 +406,3 @@ let normalize_context_set ~lbound g ctx us algs weak =
   in
   let us = normalize_opt_subst us in
     (us, algs), (ctx', Constraint.union noneqs eqs)
-
-(* let normalize_conkey = CProfile.declare_profile "normalize_context_set" *)
-(* let normalize_context_set a b c = CProfile.profile3 normalize_conkey normalize_context_set a b c *)
diff --git a/engine/univProblem.ml b/engine/univProblem.ml
index 8d6689933c..10ee601f3f 100644
--- a/engine/univProblem.ml
+++ b/engine/univProblem.ml
@@ -9,7 +9,6 @@
 (************************************************************************)
 
 open Univ
-open UnivSubst
 
 type t =
   | ULe of Universe.t * Universe.t
@@ -22,24 +21,6 @@ let is_trivial = function
   | ULe (u, v) | UEq (u, v) -> Universe.equal u v
   | ULub (u, v) | UWeak (u, v) -> Level.equal u v
 
-let subst_univs fn = function
-  | ULe (u, v) ->
-    let u' = subst_univs_universe fn u and v' = subst_univs_universe fn v in
-    if Universe.equal u' v' then None
-    else Some (ULe (u',v'))
-  | UEq (u, v) ->
-    let u' = subst_univs_universe fn u and v' = subst_univs_universe fn v in
-    if Universe.equal u' v' then None
-    else Some (ULe (u',v'))
-  | ULub (u, v) ->
-    let u' = level_subst_of fn u and v' = level_subst_of fn v in
-    if Level.equal u' v' then None
-    else Some (ULub (u',v'))
-  | UWeak (u, v) ->
-    let u' = level_subst_of fn u and v' = level_subst_of fn v in
-    if Level.equal u' v' then None
-    else Some (UWeak (u',v'))
-
 module Set = struct
   module S = Set.Make(
   struct
@@ -88,11 +69,6 @@ module Set = struct
 
   let equal x y =
     x == y || equal x y
-
-  let subst_univs subst csts =
-    fold
-      (fun c -> Option.fold_right add (subst_univs subst c))
-      csts empty
 end
 
 type 'a accumulator = Set.t -> 'a -> 'a option
diff --git a/engine/univProblem.mli b/engine/univProblem.mli
index 575f5ac847..6c7a11f529 100644
--- a/engine/univProblem.mli
+++ b/engine/univProblem.mli
@@ -32,8 +32,6 @@ module Set : sig
   include Set.S with type elt = t
 
   val pr : t -> Pp.t
-
-  val subst_univs : universe_subst_fn -> t -> t
 end
 
 type 'a accumulator = Set.t -> 'a -> 'a option
diff --git a/engine/univSubst.ml b/engine/univSubst.ml
index 330ed5d0ad..c76a4cd751 100644
--- a/engine/univSubst.ml
+++ b/engine/univSubst.ml
@@ -83,12 +83,6 @@ let subst_univs_constr subst c =
     let f = Univ.make_subst subst in
       subst_univs_fn_constr f c
 
-let subst_univs_constr =
-  if Flags.profile then
-    let subst_univs_constr_key = CProfile.declare_profile "subst_univs_constr" in
-      CProfile.profile2 subst_univs_constr_key subst_univs_constr
-  else subst_univs_constr
-
 let normalize_univ_variable ~find =
   let rec aux cur =
     let b = find cur in