diff options
Diffstat (limited to 'engine/uState.ml')
| -rw-r--r-- | engine/uState.ml | 14 |
1 files changed, 8 insertions, 6 deletions
diff --git a/engine/uState.ml b/engine/uState.ml index 4e30640e46..c28e78f7da 100644 --- a/engine/uState.ml +++ b/engine/uState.ml @@ -131,7 +131,7 @@ let of_binders b = let universe_binders ctx = fst ctx.uctx_names let instantiate_variable l b v = - try v := Univ.LMap.update l (Some b) !v + try v := Univ.LMap.set l (Some b) !v with Not_found -> assert false exception UniversesDiffer @@ -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 |