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 6aecc368e6..6969d2ba44 100644 --- a/engine/uState.ml +++ b/engine/uState.ml @@ -197,7 +197,7 @@ let process_universe_constraints ctx cstrs = | Some l -> Inr l in let equalize_variables fo l l' r r' local = - (** Assumes l = [l',0] and r = [r',0] *) + (* Assumes l = [l',0] and r = [r',0] *) let () = if is_local l' then instantiate_variable l' r vars @@ -235,8 +235,8 @@ let process_universe_constraints ctx cstrs = match cst with | ULe (l, r) -> if UGraph.check_leq univs l r then - (** Keep Prop/Set <= var around if var might be instantiated by prop or set - later. *) + (* Keep Prop/Set <= var around if var might be instantiated by prop or set + later. *) match Univ.Universe.level l, Univ.Universe.level r with | Some l, Some r -> Univ.Constraint.add (l, Univ.Le, r) local @@ -324,12 +324,14 @@ let constrain_variables diff ctx = let qualid_of_level uctx = let map, map_rev = uctx.uctx_names in fun l -> - try Libnames.qualid_of_ident (Option.get (Univ.LMap.find l map_rev).uname) + try Some (Libnames.qualid_of_ident (Option.get (Univ.LMap.find l map_rev).uname)) with Not_found | Option.IsNone -> UnivNames.qualid_of_level l let pr_uctx_level uctx l = - Libnames.pr_qualid (qualid_of_level uctx l) + match qualid_of_level uctx l with + | Some qid -> Libnames.pr_qualid qid + | None -> Univ.Level.pr l type ('a, 'b) gen_universe_decl = { univdecl_instance : 'a; (* Declared universes *) @@ -533,7 +535,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 = UnivGen.new_univ_level () in + let u = UnivGen.fresh_level () in let ctx' = Univ.ContextSet.add_universe u ctx in let uctx', pred = match rigid with |