diff options
| author |  Matthieu Sozeau <mattam@mattam.org> | 2014-06-10 16:42:21 +0200 |
|---|---|---|
| committer | Matthieu Sozeau <mattam@mattam.org> | 2014-06-10 16:42:21 +0200 |
| commit | 7f5975e33804d1e527f879539dfd14025f52a156 (patch) | |
| tree | 36be085062a6bf99ddff17c037e6d79687cef5fc /toplevel | |
| parent | b63dff21b99070e4936a799be6e2a575e42c74d4 (diff) | |
- Fix substitution of universes which needlessly hashconsed existing universes.
- More cleanup. remove unneeded functions in universes
Diffstat (limited to 'toplevel')
| -rw-r--r-- | toplevel/classes.ml | 1 |
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 |