Factorizing UState.make* through UState.from_env, to highlight the similarity.

An alternative could also be to split the initialization of the
environment and the declaration of initial "binders".

1 files changed, 3 insertions, 4 deletions

diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index e09ee150d5..cdec8b8817 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -2586,11 +2586,10 @@ let interp_univ_constraints env evd cstrs =
 
 let interp_univ_decl env decl =
   let open UState in
-  let pl : lident list = decl.univdecl_instance in
-  let evd = Evd.from_ctx (UState.make_with_initial_binders ~lbound:(Environ.universes_lbound env)
-                            (Environ.universes env) pl) in
+  let binders : lident list = decl.univdecl_instance in
+  let evd = Evd.from_env ~binders env in
   let evd, cstrs = interp_univ_constraints env evd decl.univdecl_constraints in
-  let decl = { univdecl_instance = pl;
+  let decl = { univdecl_instance = binders;
     univdecl_extensible_instance = decl.univdecl_extensible_instance;
     univdecl_constraints = cstrs;
     univdecl_extensible_constraints = decl.univdecl_extensible_constraints }