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.

---
 pretyping/univdecls.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'pretyping')

diff --git a/pretyping/univdecls.ml b/pretyping/univdecls.ml
index d16f046fab..8864be5761 100644
--- a/pretyping/univdecls.ml
+++ b/pretyping/univdecls.ml
@@ -38,7 +38,7 @@ let interp_univ_constraints env evd cstrs =
 let interp_univ_decl env decl =
   let open Misctypes in
   let pl : lident list = decl.univdecl_instance in
-  let evd = Evd.from_ctx (Evd.make_evar_universe_context env (Some pl)) in
+  let evd = Evd.from_ctx (UState.make_with_initial_binders (Environ.universes env) pl) in
   let evd, cstrs = interp_univ_constraints env evd decl.univdecl_constraints in
   let decl = { univdecl_instance = pl;
     univdecl_extensible_instance = decl.univdecl_extensible_instance;
-- 
cgit v1.2.3