From 60770e86f4ec925fce52ad3565a92beb98d253c1 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Fri, 15 Sep 2017 22:21:46 +0200
Subject: Stop exposing UState.universe_context and its Evd wrapper.

We can enforce properties through check_univ_decl, or get an arbitrary
ordered context with UState.context / Evd.to_universe_context (the
later being a new wrapper of the former).
---
 vernac/command.ml | 4 +---
 1 file changed, 1 insertion(+), 3 deletions(-)

(limited to 'vernac/command.ml')

diff --git a/vernac/command.ml b/vernac/command.ml
index 5a063f173c..80599c5345 100644
--- a/vernac/command.ml
+++ b/vernac/command.ml
@@ -1022,8 +1022,6 @@ let build_wellfounded (recname,pl,n,bl,arityc,body) poly r measure notation =
   let binders_rel = nf_evar_context !evdref binders_rel in
   let binders = nf_evar_context !evdref binders in
   let top_arity = Evarutil.nf_evar !evdref top_arity in
-  let pl, plext = Option.cata
-      (fun d -> d.univdecl_instance, d.univdecl_extensible_instance) ([],true) pl in
   let hook, recname, typ =
     if List.length binders_rel > 1 then
       let name = add_suffix recname "_func" in
@@ -1031,7 +1029,7 @@ let build_wellfounded (recname,pl,n,bl,arityc,body) poly r measure notation =
         let body = it_mkLambda_or_LetIn (mkApp (Evarutil.e_new_global evdref gr, [|make|])) binders_rel in
         let ty = it_mkProd_or_LetIn top_arity binders_rel in
         let ty = EConstr.Unsafe.to_constr ty in
-        let univs = Evd.universe_context ~names:pl ~extensible:plext !evdref in
+        let univs = Evd.check_univ_decl !evdref decl in
         (*FIXME poly? *)
         let ce = definition_entry ~poly ~types:ty ~univs (EConstr.to_constr !evdref body) in
         (** FIXME: include locality *)
-- 
cgit v1.2.3