aboutsummaryrefslogtreecommitdiffhomepage
path: root/vernac
diff options
context:
space:
mode:
Diffstat (limited to 'vernac')
-rw-r--r--vernac/class.ml2
-rw-r--r--vernac/command.ml4
-rw-r--r--vernac/indschemes.ml2
-rw-r--r--vernac/lemmas.ml15
-rw-r--r--vernac/obligations.ml13
5 files changed, 18 insertions, 18 deletions
diff --git a/vernac/class.ml b/vernac/class.ml
index e59482b71..68fd22cb6 100644
--- a/vernac/class.ml
+++ b/vernac/class.ml
@@ -212,7 +212,7 @@ let build_id_coercion idf_opt source poly =
Id.of_string ("Id_"^(ident_key_of_class source)^"_"^
(ident_key_of_class cl))
in
- let univs = Evd.universe_context ~names:[] ~extensible:true sigma in
+ let univs = Evd.to_universe_context sigma in
let constr_entry = (* Cast is necessary to express [val_f] is identity *)
DefinitionEntry
(definition_entry ~types:typ_f ~poly ~univs
diff --git a/vernac/command.ml b/vernac/command.ml
index 5a063f173..80599c534 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 *)
diff --git a/vernac/indschemes.ml b/vernac/indschemes.ml
index 58f39e303..c728c2671 100644
--- a/vernac/indschemes.ml
+++ b/vernac/indschemes.ml
@@ -109,7 +109,7 @@ let _ =
let define id internal ctx c t =
let f = declare_constant ~internal in
- let univs = Evd.universe_context ~names:[] ~extensible:true ctx in
+ let univs = Evd.to_universe_context ctx in
let univs =
if Flags.is_universe_polymorphism () then Polymorphic_const_entry univs
else Monomorphic_const_entry univs
diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml
index cd30c7a68..71d80c4db 100644
--- a/vernac/lemmas.ml
+++ b/vernac/lemmas.ml
@@ -49,7 +49,8 @@ let retrieve_first_recthm uctx = function
(NamedDecl.get_value (Global.lookup_named id),variable_opacity id)
| ConstRef cst ->
let cb = Global.lookup_constant cst in
- let uctx = UState.universe_context ~names:[] ~extensible:true uctx in
+ (* we get the right order somehow but surely it could be enforced in a better way *)
+ let uctx = UState.context uctx in
let inst = Univ.UContext.instance uctx in
let map (c, ctx) = Vars.subst_instance_constr inst c in
(Option.map map (Global.body_of_constant_body cb), is_opaque cb)
@@ -420,8 +421,8 @@ let start_proof_with_initialization kind ctx decl recguard thms snl hook =
let body,opaq = retrieve_first_recthm ctx ref in
let subst = Evd.evar_universe_context_subst ctx in
let norm c = Universes.subst_opt_univs_constr subst c in
- let ctx = Evd.check_univ_decl (Evd.from_ctx ctx) decl in
- let body = Option.map norm body in
+ let ctx = UState.check_univ_decl ctx decl in
+ let body = Option.map norm body in
List.map_i (save_remaining_recthms kind norm ctx body opaq) 1 other_thms in
let thms_data = (strength,ref,imps)::other_thms_data in
List.iter (fun (strength,ref,imps) ->
@@ -453,9 +454,9 @@ let start_proof_com ?inference_hook kind thms hook =
let evd, nf = Evarutil.nf_evars_and_universes !evdref in
let thms = List.map (fun (n, (t, info)) -> (n, (nf t, info))) thms in
let () =
- if not decl.Misctypes.univdecl_extensible_instance then
- ignore (Evd.universe_context evd ~names:decl.Misctypes.univdecl_instance ~extensible:false)
- else ()
+ let open Misctypes in
+ if not (decl.univdecl_extensible_instance && decl.univdecl_extensible_constraints) then
+ ignore (Evd.check_univ_decl evd decl)
in
let evd =
if pi2 kind then evd
@@ -490,7 +491,7 @@ let save_proof ?proof = function
if const_entry_type = None then
user_err Pp.(str "Admitted requires an explicit statement");
let typ = Option.get const_entry_type in
- let ctx = Evd.evar_context_universe_context (fst universes) in
+ let ctx = UState.context (fst universes) in
let sec_vars = if !keep_admitted_vars then const_entry_secctx else None in
Admitted(id, k, (sec_vars, pi2 k, (typ, ctx), None), universes)
| None ->
diff --git a/vernac/obligations.ml b/vernac/obligations.ml
index 216801811..43af8968f 100644
--- a/vernac/obligations.ml
+++ b/vernac/obligations.ml
@@ -479,7 +479,7 @@ let declare_definition prg =
let ce =
definition_entry ~fix_exn
~opaque ~types:(nf typ) ~poly:(pi2 prg.prg_kind)
- ~univs:(Evd.evar_context_universe_context prg.prg_ctx) (nf body)
+ ~univs:(UState.context prg.prg_ctx) (nf body)
in
let () = progmap_remove prg in
let ubinders = UState.universe_binders prg.prg_ctx in
@@ -549,7 +549,7 @@ let declare_mutual_definition l =
mk_proof (mkCoFix (i,fixdecls))) 0 l
in
(* Declare the recursive definitions *)
- let ctx = Evd.evar_context_universe_context first.prg_ctx in
+ let ctx = UState.context first.prg_ctx in
let fix_exn = Hook.get get_fix_exn () in
let kns = List.map4 (DeclareDef.declare_fix ~opaque (local, poly, kind) Universes.empty_binders ctx)
fixnames fixdecls fixtypes fiximps in
@@ -855,7 +855,7 @@ let obligation_terminator name num guard hook auto pf =
| (_, status), Vernacexpr.Transparent -> status
in
let obl = { obl with obl_status = false, status } in
- let uctx = Evd.evar_context_universe_context ctx in
+ let uctx = UState.context ctx in
let (_, obl) = declare_obligation prg obl body ty uctx in
let obls = Array.copy obls in
let _ = obls.(num) <- obl in
@@ -890,7 +890,8 @@ in
let ctx' = Evd.merge_universe_subst evd (Evd.universe_subst (Evd.from_ctx ctx')) in
Univ.Instance.empty, Evd.evar_universe_context ctx'
else
- let uctx = UState.universe_context ~names:[] ~extensible:true ctx' in
+ (* We get the right order somehow, but surely it could be enforced in a clearer way. *)
+ let uctx = UState.context ctx' in
Univ.UContext.instance uctx, ctx'
in
let obl = { obl with obl_body = Some (DefinedObl (cst, inst)) } in
@@ -969,7 +970,7 @@ and solve_obligation_by_tac prg obls i tac =
solve_by_tac obl.obl_name (evar_of_obligation obl) tac
(pi2 prg.prg_kind) (Evd.evar_universe_context evd)
in
- let uctx = Evd.evar_context_universe_context ctx in
+ let uctx = UState.context ctx in
let prg = {prg with prg_ctx = ctx} in
let def, obl' = declare_obligation prg obl t ty uctx in
obls.(i) <- obl';
@@ -1120,7 +1121,7 @@ let admit_prog prg =
match x.obl_body with
| None ->
let x = subst_deps_obl obls x in
- let ctx = Evd.evar_context_universe_context prg.prg_ctx in
+ let ctx = UState.context prg.prg_ctx in
let kn = Declare.declare_constant x.obl_name ~local:true
(ParameterEntry (None,false,(x.obl_type,ctx),None), IsAssumption Conjectural)
in
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-27 05:57:15 +0000