aboutsummaryrefslogtreecommitdiffhomepage
path: root/toplevel/classes.ml
diff options
context:
space:
mode:
Diffstat (limited to 'toplevel/classes.ml')
-rw-r--r--toplevel/classes.ml1
1 files changed, 0 insertions, 1 deletions
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