diff options
Diffstat (limited to 'interp')
| -rw-r--r-- | interp/declare.ml | 8 |
1 files changed, 2 insertions, 6 deletions
diff --git a/interp/declare.ml b/interp/declare.ml index 0c9d26dd01..a809a856b9 100644 --- a/interp/declare.ml +++ b/interp/declare.ml @@ -469,7 +469,7 @@ type universe_source = | QualifiedUniv of Id.t (* global universe introduced by some global value *) | UnqualifiedUniv (* other global universe *) -type universe_name_decl = universe_source * (Id.t * Univ.Level.Qualid.t) list +type universe_name_decl = universe_source * (Id.t * Univ.Level.UGlobal.t) list let check_exists sp = if Nametab.exists_universe sp then @@ -540,11 +540,7 @@ let do_universe poly l = user_err ~hdr:"Constraint" (str"Cannot declare polymorphic universes outside sections") in - let l = - List.map (fun {CAst.v=id} -> - let lev = UnivGen.new_univ_id () in - (id, Univ.Level.Qualid.make (Global.current_dirpath ()) lev)) l - in + let l = List.map (fun {CAst.v=id} -> (id, UnivGen.new_univ_global ())) l in let ctx = List.fold_left (fun ctx (_,qid) -> Univ.LSet.add (Univ.Level.make qid) ctx) Univ.LSet.empty l, Univ.Constraint.empty in |