diff options
Diffstat (limited to 'toplevel/vernacentries.ml')
| -rw-r--r-- | toplevel/vernacentries.ml | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index 8ae6ac2bc..c07c756c0 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -76,9 +76,8 @@ let show_universes () = let gls = Proof.V82.subgoals pfts in let sigma = gls.Evd.sigma in let ctx = Evd.universe_context_set (Evd.nf_constraints sigma) in - let cstrs = Univ.merge_constraints (Univ.ContextSet.constraints ctx) Univ.empty_universes in msg_notice (Evd.pr_evar_universe_context (Evd.evar_universe_context sigma)); - msg_notice (str"Normalized constraints: " ++ Univ.pr_universes (Evd.pr_evd_level sigma) cstrs) + msg_notice (str"Normalized constraints: " ++ Univ.pr_universe_context_set (Evd.pr_evd_level sigma) ctx) let show_prooftree () = (* Spiwack: proof tree is currently not working *) @@ -1185,8 +1184,9 @@ let default_env () = { let vernac_reserve bl = let sb_decl = (fun (idl,c) -> let env = Global.env() in - let t,ctx = Constrintern.interp_type env Evd.empty c in - let t = Detyping.detype false [] env Evd.empty t in + let sigma = Evd.from_env env in + let t,ctx = Constrintern.interp_type env sigma c in + let t = Detyping.detype false [] env (Evd.from_ctx ctx) t in let t = Notation_ops.notation_constr_of_glob_constr (default_env ()) t in Reserve.declare_reserved_type idl t) in List.iter sb_decl bl |