From 5d926b0279f70250db1ee54edcdb4e855ac96f0f Mon Sep 17 00:00:00 2001 From: Gaëtan Gilbert Date: Fri, 2 Mar 2018 14:58:00 +0100 Subject: Deprecate UState aliases in Evd. --- printing/prettyp.ml | 4 ++-- printing/printmod.ml | 4 ++-- 2 files changed, 4 insertions(+), 4 deletions(-) (limited to 'printing') diff --git a/printing/prettyp.ml b/printing/prettyp.ml index 3682b7c25..9da94e42a 100644 --- a/printing/prettyp.ml +++ b/printing/prettyp.ml @@ -94,7 +94,7 @@ let print_ref reduce ref udecl = let env = Global.env () in let bl = Universes.universe_binders_with_opt_names ref (Array.to_list (Univ.Instance.to_array inst)) udecl in - let sigma = Evd.from_ctx (Evd.evar_universe_context_of_binders bl) in + let sigma = Evd.from_ctx (UState.of_binders bl) in let inst = if Global.is_polymorphic ref then Printer.pr_universe_instance sigma univs else mt () @@ -593,7 +593,7 @@ let print_constant with_values sep sp udecl = Array.to_list (Instance.to_array inst) in let ctx = - Evd.evar_universe_context_of_binders + UState.of_binders (Universes.universe_binders_with_opt_names (ConstRef sp) ulist udecl) in let env = Global.env () and sigma = Evd.from_ctx ctx in diff --git a/printing/printmod.ml b/printing/printmod.ml index 43796ec61..e076c10f3 100644 --- a/printing/printmod.ml +++ b/printing/printmod.ml @@ -141,7 +141,7 @@ let print_mutual_inductive env mind mib udecl = else [] in let bl = Universes.universe_binders_with_opt_names (IndRef (mind, 0)) univs udecl in - let sigma = Evd.from_ctx (Evd.evar_universe_context_of_binders bl) in + let sigma = Evd.from_ctx (UState.of_binders bl) in hov 0 (Printer.pr_polymorphic (Declareops.inductive_is_polymorphic mib) ++ Printer.pr_cumulative (Declareops.inductive_is_polymorphic mib) @@ -185,7 +185,7 @@ let print_record env mind mib udecl = let envpar = push_rel_context params env in let bl = Universes.universe_binders_with_opt_names (IndRef (mind,0)) (Array.to_list (Univ.Instance.to_array u)) udecl in - let sigma = Evd.from_ctx (Evd.evar_universe_context_of_binders bl) in + let sigma = Evd.from_ctx (UState.of_binders bl) in let keyword = let open Declarations in match mib.mind_finite with -- cgit v1.2.3