diff options
| author | Gaëtan Gilbert | 2017-09-15 22:21:46 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert | 2017-11-24 19:18:56 +0100 |
| commit | 60770e86f4ec925fce52ad3565a92beb98d253c1 (patch) | |
| tree | 427bc507cffa5848bead327b04547154c8d23591 /vernac/command.ml | |
| parent | a5feb9687819c5e7ef0db6e7b74d0e236a296674 (diff) | |
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).
Diffstat (limited to 'vernac/command.ml')
| -rw-r--r-- | vernac/command.ml | 4 |
1 files changed, 1 insertions, 3 deletions
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 *) |