diff options
| author |  Matthieu Sozeau <mattam@mattam.org> | 2017-12-01 10:11:41 +0100 |
|---|---|---|
| committer | Matthieu Sozeau <mattam@mattam.org> | 2017-12-01 10:16:49 +0100 |
| commit | 20c98eab851210702b39e1c66e005acfc351d8dd (patch) | |
| tree | 957aab7aadfda8c10f251ff9d83f3f5b05c07dc5 /engine/uState.ml | |
| parent | 0048cbe810c82a775558c14cd7fcae644e205c51 (diff) | |
Proper nametab handling of global universe names
They are now bound at the library + module level and can be qualified
and shadowed according to the usual rules of qualified names.
Parsing and printing of universes "u+n" done as well.
In sections, global universes are discharged as well, checking that
they can be defined globally when they are introduced
Diffstat (limited to 'engine/uState.ml')
| -rw-r--r-- | engine/uState.ml | 12 |
1 files changed, 7 insertions, 5 deletions
diff --git a/engine/uState.ml b/engine/uState.ml index 4e30640e4..511d55328 100644 --- a/engine/uState.ml +++ b/engine/uState.ml @@ -263,13 +263,15 @@ let constrain_variables diff ctx = in { ctx with uctx_local = (univs, local); uctx_univ_variables = vars } - -let pr_uctx_level uctx = +let reference_of_level uctx = let map, map_rev = uctx.uctx_names in fun l -> - try Id.print (Option.get (Univ.LMap.find l map_rev).uname) + try Libnames.Ident (Loc.tag @@ Option.get (Univ.LMap.find l map_rev).uname) with Not_found | Option.IsNone -> - Universes.pr_with_global_universes l + Universes.reference_of_level l + +let pr_uctx_level uctx l = + Libnames.pr_reference (reference_of_level uctx l) type universe_decl = (Names.Id.t Loc.located list, Univ.Constraint.t) Misctypes.gen_universe_decl @@ -430,7 +432,7 @@ let emit_side_effects eff u = let new_univ_variable ?loc rigid name ({ uctx_local = ctx; uctx_univ_variables = uvars; uctx_univ_algebraic = avars} as uctx) = - let u = Universes.new_univ_level (Global.current_dirpath ()) in + let u = Universes.new_univ_level () in let ctx' = Univ.ContextSet.add_universe u ctx in let uctx', pred = match rigid with |