From 7f5975e33804d1e527f879539dfd14025f52a156 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau <mattam@mattam.org>
Date: Tue, 10 Jun 2014 16:42:21 +0200
Subject: - Fix substitution of universes which needlessly hashconsed existing
 universes. - More cleanup. remove unneeded functions in universes

---
 toplevel/classes.ml | 1 -
 1 file changed, 1 deletion(-)

(limited to 'toplevel')

diff --git a/toplevel/classes.ml b/toplevel/classes.ml
index 99c3e977c..56f9cb564 100644
--- a/toplevel/classes.ml
+++ b/toplevel/classes.ml
@@ -339,7 +339,6 @@ let context l =
   in
   let uctx = Evd.universe_context_set !evars in
   let fn status (id, b, t) =
-    (* let uctx = Universes.shrink_universe_context uctx (Universes.universes_of_constr t) in *)
     if Lib.is_modtype () && not (Lib.sections_are_opened ()) then
       let uctx = Univ.ContextSet.to_context uctx in	
       let decl = (ParameterEntry (None,false,(t,uctx),None), IsAssumption Logical) in
-- 
cgit v1.2.3