aboutsummaryrefslogtreecommitdiffhomepage
path: root/printing/prettyp.ml
diff options
context:
space:
mode:
authorGravatar Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>2018-03-02 14:58:00 +0100
committerGravatar Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>2018-03-06 13:41:24 +0100
commit5d926b0279f70250db1ee54edcdb4e855ac96f0f (patch)
tree06dc436ba2d41764b5bbe48c311bdaeaf5c1514c /printing/prettyp.ml
parent67a28c487fc64e2c0f8271b77d0c9db0cd82fa92 (diff)
Deprecate UState aliases in Evd.
Diffstat (limited to 'printing/prettyp.ml')
-rw-r--r--printing/prettyp.ml4
1 files changed, 2 insertions, 2 deletions
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