From 2b7ccb235b503f4c978009c2d7908d305cf85925 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Mon, 21 Jul 2014 18:31:41 +0200
Subject: Cleanup substitution inside universe instances, only done through
 subst_fn now, and disable hashconsing of substituted instances which had a
 huge performance penalty in general. They are hashconsed when put in the
 environment only now.

---
 checker/term.ml | 10 ----------
 1 file changed, 10 deletions(-)

(limited to 'checker')

diff --git a/checker/term.ml b/checker/term.ml
index 3372f9b6c3..e8cdb03e99 100644
--- a/checker/term.ml
+++ b/checker/term.ml
@@ -397,16 +397,6 @@ let eq_constr m n = eq_constr m n (* to avoid tracing a recursive fun *)
 
 (* Universe substitutions *)
 
-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')
-
 let map_constr f c = map_constr_with_binders (fun x -> x) (fun _ c -> f c) 0 c
 
 let subst_univs_fn_constr f c =
-- 
cgit v1.2.3