diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2018-03-08 21:22:59 +0100 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2018-03-08 21:22:59 +0100 |
| commit | a40fb961c8ffeeb03769404cacda8bd6cff17417 (patch) | |
| tree | 7105d621bc16f825c1f309e3d5b7720b1b1513ec /pretyping | |
| parent | 3875a525ee1e075be9f0eb1f17c74726e9f38b43 (diff) | |
| parent | 66973ce17e32a3c692a5b0032f38300ec8cc36d3 (diff) | |
Merge PR #6893: Cleanup UState API usage
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/univdecls.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/pretyping/univdecls.ml b/pretyping/univdecls.ml index d16f046fa..8864be576 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; |