aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--API/API.mli3
-rw-r--r--engine/evd.ml2
-rw-r--r--engine/evd.mli7
-rw-r--r--engine/uState.ml8
-rw-r--r--engine/uState.mli6
-rw-r--r--plugins/funind/functional_principles_types.ml2
-rw-r--r--plugins/funind/recdef.ml2
-rw-r--r--plugins/ltac/rewrite.ml2
-rw-r--r--plugins/setoid_ring/newring.ml2
-rw-r--r--printing/printer.ml7
-rw-r--r--printing/printer.mli1
-rw-r--r--proofs/proof_global.ml10
-rw-r--r--tactics/leminv.ml4
-rw-r--r--vernac/class.ml2
-rw-r--r--vernac/classes.ml8
-rw-r--r--vernac/command.ml48
-rw-r--r--vernac/indschemes.ml2
-rw-r--r--vernac/lemmas.ml12
-rw-r--r--vernac/obligations.ml15
-rw-r--r--vernac/record.ml5
-rw-r--r--vernac/vernacentries.ml6
21 files changed, 87 insertions, 67 deletions
diff --git a/API/API.mli b/API/API.mli
index 63c675221..889050d90 100644
--- a/API/API.mli
+++ b/API/API.mli
@@ -2882,7 +2882,8 @@ sig
val evar_ident : evar -> evar_map -> Names.Id.t option
val extract_all_conv_pbs : evar_map -> evar_map * evar_constraint list
val universe_context : names:(Names.Id.t Loc.located) list -> extensible:bool -> evar_map ->
- Universes.universe_binders * Univ.UContext.t
+ Univ.UContext.t
+ val universe_binders : evar_map -> Universes.universe_binders
val nf_constraints : evar_map -> evar_map
val from_ctx : UState.t -> evar_map
diff --git a/engine/evd.ml b/engine/evd.ml
index ca1196b94..67ae73ceb 100644
--- a/engine/evd.ml
+++ b/engine/evd.ml
@@ -936,6 +936,8 @@ let universe_of_name evd s = UState.universe_of_name evd.universes s
let add_universe_name evd s l =
{ evd with universes = UState.add_universe_name evd.universes s l }
+let universe_binders evd = UState.universe_binders evd.universes
+
let universes evd = UState.ugraph evd.universes
let update_sigma_env evd env =
diff --git a/engine/evd.mli b/engine/evd.mli
index 36c399e98..b6157202d 100644
--- a/engine/evd.mli
+++ b/engine/evd.mli
@@ -509,7 +509,8 @@ val restrict_universe_context : evar_map -> Univ.LSet.t -> evar_map
val universe_of_name : evar_map -> Id.t -> Univ.Level.t
val add_universe_name : evar_map -> Id.t -> Univ.Level.t -> evar_map
-val add_constraints_context : UState.t ->
+val universe_binders : evar_map -> Universes.universe_binders
+val add_constraints_context : UState.t ->
Univ.constraints -> UState.t
@@ -552,12 +553,12 @@ val check_leq : evar_map -> Univ.Universe.t -> Univ.Universe.t -> bool
val evar_universe_context : evar_map -> UState.t
val universe_context_set : evar_map -> Univ.ContextSet.t
val universe_context : names:(Id.t located) list -> extensible:bool -> evar_map ->
- Universes.universe_binders * Univ.UContext.t
+ Univ.UContext.t
val universe_subst : evar_map -> Universes.universe_opt_subst
val universes : evar_map -> UGraph.t
val check_univ_decl : evar_map -> UState.universe_decl ->
- Universes.universe_binders * Univ.UContext.t
+ Univ.UContext.t
val merge_universe_context : evar_map -> UState.t -> evar_map
val set_universe_context : evar_map -> UState.t -> evar_map
diff --git a/engine/uState.ml b/engine/uState.ml
index 498d73fd3..282acb3d6 100644
--- a/engine/uState.ml
+++ b/engine/uState.ml
@@ -114,6 +114,8 @@ let of_binders b =
in
{ ctx with uctx_names = b, rmap }
+let universe_binders ctx = fst ctx.uctx_names
+
let instantiate_variable l b v =
try v := Univ.LMap.update l (Some b) !v
with Not_found -> assert false
@@ -291,7 +293,7 @@ let universe_context ~names ~extensible uctx =
let inst = Univ.Instance.of_array inst in
let ctx = Univ.UContext.make (inst,
Univ.ContextSet.constraints uctx.uctx_local) in
- fst uctx.uctx_names, ctx
+ ctx
let check_implication uctx cstrs ctx =
let gr = initial_graph uctx in
@@ -303,14 +305,14 @@ let check_implication uctx cstrs ctx =
let check_univ_decl uctx decl =
let open Misctypes in
- let pl, ctx = universe_context
+ let ctx = universe_context
~names:decl.univdecl_instance
~extensible:decl.univdecl_extensible_instance
uctx
in
if not decl.univdecl_extensible_constraints then
check_implication uctx decl.univdecl_constraints ctx;
- pl, ctx
+ ctx
let restrict ctx vars =
let uctx' = Univops.restrict_universe_context ctx.uctx_local vars in
diff --git a/engine/uState.mli b/engine/uState.mli
index 7f2357a68..38af08f91 100644
--- a/engine/uState.mli
+++ b/engine/uState.mli
@@ -32,6 +32,8 @@ val of_context_set : Univ.ContextSet.t -> t
val of_binders : Universes.universe_binders -> t
+val universe_binders : t -> Universes.universe_binders
+
(** {5 Projections} *)
val context_set : t -> Univ.ContextSet.t
@@ -135,12 +137,12 @@ val normalize : t -> t
Also return the association list of universe names and universes
(including those not in [names]). *)
val universe_context : names:(Id.t Loc.located) list -> extensible:bool -> t ->
- Universes.universe_binders * Univ.UContext.t
+ Univ.UContext.t
type universe_decl =
(Names.Id.t Loc.located list, Univ.Constraint.t) Misctypes.gen_universe_decl
-val check_univ_decl : t -> universe_decl -> Universes.universe_binders * Univ.UContext.t
+val check_univ_decl : t -> universe_decl -> Univ.UContext.t
(** {5 TODO: Document me} *)
diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml
index 996e2b6af..d5bff57af 100644
--- a/plugins/funind/functional_principles_types.ml
+++ b/plugins/funind/functional_principles_types.ml
@@ -348,7 +348,7 @@ let generate_functional_principle (evd: Evd.evar_map ref)
let evd',value = change_property_sort evd' s new_principle_type new_princ_name in
let evd' = fst (Typing.type_of ~refresh:true (Global.env ()) evd' (EConstr.of_constr value)) in
(* Pp.msgnl (str "new principle := " ++ pr_lconstr value); *)
- let univs = (snd (Evd.universe_context ~names:[] ~extensible:true evd')) in
+ let univs = Evd.universe_context ~names:[] ~extensible:true evd' in
let ce = Declare.definition_entry ~poly:(Flags.is_universe_polymorphism ()) ~univs value in
ignore(
Declare.declare_constant
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index 3089ec470..63896bb56 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -1556,7 +1556,7 @@ let recursive_definition is_mes function_name rec_impls type_of_f r rec_arg_num
let functional_id = add_suffix function_name "_F" in
let term_id = add_suffix function_name "_terminate" in
let functional_ref =
- let ctx = (snd (Evd.universe_context ~names:[] ~extensible:true evm)) in
+ let ctx = Evd.universe_context ~names:[] ~extensible:true evm in
declare_fun functional_id (IsDefinition Decl_kinds.Definition) ~ctx res
in
(* Refresh the global universes, now including those of _F *)
diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml
index 14b0742a7..2eb660219 100644
--- a/plugins/ltac/rewrite.ml
+++ b/plugins/ltac/rewrite.ml
@@ -1884,7 +1884,7 @@ let declare_projection n instance_id r =
in it_mkProd_or_LetIn ccl ctx
in
let typ = it_mkProd_or_LetIn typ ctx in
- let pl, ctx = Evd.universe_context ~names:[] ~extensible:true sigma in
+ let ctx = Evd.universe_context ~names:[] ~extensible:true sigma in
let typ = EConstr.to_constr sigma typ in
let term = EConstr.to_constr sigma term in
let cst =
diff --git a/plugins/setoid_ring/newring.ml b/plugins/setoid_ring/newring.ml
index 1c3bdb958..a37b35b3d 100644
--- a/plugins/setoid_ring/newring.ml
+++ b/plugins/setoid_ring/newring.ml
@@ -220,7 +220,7 @@ let exec_tactic env evd n f args =
let gls = Proofview.V82.of_tactic (Tacinterp.eval_tactic_ist ist (ltac_call f (args@[getter]))) gl in
let evd, nf = Evarutil.nf_evars_and_universes (Refiner.project gls) in
let nf c = nf (constr_of c) in
- Array.map nf !tactic_res, snd (Evd.universe_context ~names:[] ~extensible:true evd)
+ Array.map nf !tactic_res, Evd.universe_context ~names:[] ~extensible:true evd
let stdlib_modules =
[["Coq";"Setoids";"Setoid"];
diff --git a/printing/printer.ml b/printing/printer.ml
index d7bb0460d..4d5cfcba3 100644
--- a/printing/printer.ml
+++ b/printing/printer.ml
@@ -256,6 +256,13 @@ let safe_pr_constr t =
let (sigma, env) = Pfedit.get_current_context () in
safe_pr_constr_env env sigma t
+let pr_universe_ctx_set sigma c =
+ if !Detyping.print_universes && not (Univ.ContextSet.is_empty c) then
+ fnl()++pr_in_comment (fun c -> v 0
+ (Univ.pr_universe_context_set (Termops.pr_evd_level sigma) c)) c
+ else
+ mt()
+
let pr_universe_ctx sigma c =
if !Detyping.print_universes && not (Univ.UContext.is_empty c) then
fnl()++pr_in_comment (fun c -> v 0
diff --git a/printing/printer.mli b/printing/printer.mli
index e014baa2c..a3d0eaac2 100644
--- a/printing/printer.mli
+++ b/printing/printer.mli
@@ -121,6 +121,7 @@ val pr_polymorphic : bool -> Pp.t
val pr_cumulative : bool -> bool -> Pp.t
val pr_universe_instance : evar_map -> Univ.UContext.t -> Pp.t
val pr_universe_ctx : evar_map -> Univ.UContext.t -> Pp.t
+val pr_universe_ctx_set : evar_map -> Univ.ContextSet.t -> Pp.t
val pr_cumulativity_info : evar_map -> Univ.CumulativityInfo.t -> Pp.t
(** Printing global references using names as short as possible *)
diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml
index fdc9a236b..9faff3211 100644
--- a/proofs/proof_global.ml
+++ b/proofs/proof_global.ml
@@ -331,8 +331,8 @@ let close_proof ~keep_body_ucst_separate ?feedback_id ~now
let initial_euctx = Proof.initial_euctx proof in
let fpl, univs = Future.split2 fpl in
let universes = if poly || now then Future.force univs else initial_euctx in
- let binders, univctx = Evd.check_univ_decl (Evd.from_ctx universes) universe_decl in
- let binders = if poly then Some binders else None in
+ let univctx = Evd.check_univ_decl (Evd.from_ctx universes) universe_decl in
+ let binders = if poly then Some (UState.universe_binders universes) else None in
(* Because of dependent subgoals at the beginning of proofs, we could
have existential variables in the initial types of goals, we need to
normalise them for the kernel. *)
@@ -360,7 +360,7 @@ let close_proof ~keep_body_ucst_separate ?feedback_id ~now
the body. So we keep the two sets distinct. *)
let used_univs = Univ.LSet.union used_univs_body used_univs_typ in
let ctx_body = UState.restrict ctx used_univs in
- let _, univs = Evd.check_univ_decl (Evd.from_ctx ctx_body) universe_decl in
+ let univs = Evd.check_univ_decl (Evd.from_ctx ctx_body) universe_decl in
(initunivs, typ), ((body, Univ.ContextSet.of_context univs), eff)
else
(* Since the proof is computed now, we can simply have 1 set of
@@ -370,7 +370,7 @@ let close_proof ~keep_body_ucst_separate ?feedback_id ~now
TODO: check if restrict is really necessary now. *)
let used_univs = Univ.LSet.union used_univs_body used_univs_typ in
let ctx = UState.restrict universes used_univs in
- let _, univs = Evd.check_univ_decl (Evd.from_ctx ctx) universe_decl in
+ let univs = Evd.check_univ_decl (Evd.from_ctx ctx) universe_decl in
(univs, typ), ((body, Univ.ContextSet.empty), eff)
in
fun t p -> Future.split2 (Future.chain p (make_body t))
@@ -383,7 +383,7 @@ let close_proof ~keep_body_ucst_separate ?feedback_id ~now
the declaration as well. If the declaration is non-extensible,
this will prevent the body from adding universes and constraints. *)
let bodyunivs = constrain_variables univctx (Future.force univs) in
- let _, univs = Evd.check_univ_decl (Evd.from_ctx bodyunivs) universe_decl in
+ let univs = Evd.check_univ_decl (Evd.from_ctx bodyunivs) universe_decl in
(pt,Univ.ContextSet.of_context univs),eff)
in
let entry_fn p (_, t) =
diff --git a/tactics/leminv.ml b/tactics/leminv.ml
index 62f3866de..4d1b271d6 100644
--- a/tactics/leminv.ml
+++ b/tactics/leminv.ml
@@ -235,9 +235,9 @@ let inversion_scheme env sigma t sort dep_option inv_op =
p, Evd.universe_context ~names:[] ~extensible:true sigma
let add_inversion_lemma name env sigma t sort dep inv_op =
- let invProof, ctx = inversion_scheme env sigma t sort dep inv_op in
+ let invProof, univs = inversion_scheme env sigma t sort dep inv_op in
let entry = definition_entry ~poly:(Flags.use_polymorphic_flag ())
- ~univs:(snd ctx) invProof in
+ ~univs invProof in
let _ = declare_constant name (DefinitionEntry entry, IsProof Lemma) in
()
diff --git a/vernac/class.ml b/vernac/class.ml
index 44f20a088..e59482b71 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 = (snd (Evd.universe_context ~names:[] ~extensible:true sigma)) in
+ let univs = Evd.universe_context ~names:[] ~extensible:true 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/classes.ml b/vernac/classes.ml
index ed37bab6d..6f5f96ee2 100644
--- a/vernac/classes.ml
+++ b/vernac/classes.ml
@@ -119,14 +119,14 @@ let declare_instance_constant k info global imps ?hook id decl poly evm term ter
(Univops.universes_of_constr term) in
Evd.restrict_universe_context evm levels
in
- let pl, uctx = Evd.check_univ_decl evm decl in
+ let uctx = Evd.check_univ_decl evm decl in
let entry =
Declare.definition_entry ~types:termtype ~poly ~univs:uctx term
in
let cdecl = (DefinitionEntry entry, kind) in
let kn = Declare.declare_constant id cdecl in
Declare.definition_message id;
- Universes.register_universe_binders (ConstRef kn) pl;
+ Universes.register_universe_binders (ConstRef kn) (Evd.universe_binders evm);
instance_hook k info global imps ?hook (ConstRef kn);
id
@@ -203,12 +203,12 @@ let new_instance ?(abstract=false) ?(global=false) ?(refine= !refine_instance)
nf t
in
Pretyping.check_evars env Evd.empty !evars (EConstr.of_constr termtype);
- let pl, ctx = Evd.check_univ_decl !evars decl in
+ let ctx = Evd.check_univ_decl !evars decl in
let cst = Declare.declare_constant ~internal:Declare.InternalTacticRequest id
(ParameterEntry
(None,poly,(termtype,ctx),None), Decl_kinds.IsAssumption Decl_kinds.Logical)
in
- Universes.register_universe_binders (ConstRef cst) pl;
+ Universes.register_universe_binders (ConstRef cst) (Evd.universe_binders !evars);
instance_hook k pri global imps ?hook (ConstRef cst); id
end
else (
diff --git a/vernac/command.ml b/vernac/command.ml
index 5d83de070..5a063f173 100644
--- a/vernac/command.ml
+++ b/vernac/command.ml
@@ -107,8 +107,9 @@ let interp_definition pl bl p red_option c ctypopt =
let body = nf (it_mkLambda_or_LetIn c ctx) in
let vars = Univops.universes_of_constr body in
let evd = Evd.restrict_universe_context !evdref vars in
- let pl, uctx = Evd.check_univ_decl evd decl in
- imps1@(Impargs.lift_implicits nb_args imps2), pl,
+ let uctx = Evd.check_univ_decl evd decl in
+ let binders = Evd.universe_binders evd in
+ imps1@(Impargs.lift_implicits nb_args imps2), binders,
definition_entry ~univs:uctx ~poly:p body
| Some ctyp ->
let ty, impsty = interp_type_evars_impls ~impls env_bl evdref ctyp in
@@ -133,8 +134,9 @@ let interp_definition pl bl p red_option c ctypopt =
let vars = Univ.LSet.union (Univops.universes_of_constr body)
(Univops.universes_of_constr typ) in
let ctx = Evd.restrict_universe_context !evdref vars in
- let pl, uctx = Evd.check_univ_decl ctx decl in
- imps1@(Impargs.lift_implicits nb_args impsty), pl,
+ let uctx = Evd.check_univ_decl ctx decl in
+ let binders = Evd.universe_binders evd in
+ imps1@(Impargs.lift_implicits nb_args impsty), binders,
definition_entry ~types:typ ~poly:p
~univs:uctx body
in
@@ -277,9 +279,10 @@ let do_assumptions_bound_univs coe kind nl id pl c =
let ty = nf ty in
let vars = Univops.universes_of_constr ty in
let evd = Evd.restrict_universe_context !evdref vars in
- let pl, uctx = Evd.check_univ_decl evd decl in
+ let uctx = Evd.check_univ_decl evd decl in
+ let binders = Evd.universe_binders evd in
let uctx = Univ.ContextSet.of_context uctx in
- let (_, _, st) = declare_assumption coe kind (ty, uctx) pl impls false nl id in
+ let (_, _, st) = declare_assumption coe kind (ty, uctx) binders impls false nl id in
st
let do_assumptions kind nl l = match l with
@@ -576,7 +579,7 @@ let interp_mutual_inductive (paramsl,indl) notations cum poly prv finite =
let constructors = List.map (fun (idl,cl,impsl) -> (idl,List.map nf' cl,impsl)) constructors in
let ctx_params = Context.Rel.map nf ctx_params in
let evd = !evdref in
- let pl, uctx = Evd.check_univ_decl evd decl in
+ let uctx = Evd.check_univ_decl evd decl in
List.iter (fun c -> check_evars env_params Evd.empty evd (EConstr.of_constr c)) arities;
Context.Rel.iter (fun c -> check_evars env0 Evd.empty evd (EConstr.of_constr c)) ctx_params;
List.iter (fun (_,ctyps,_) ->
@@ -617,7 +620,7 @@ let interp_mutual_inductive (paramsl,indl) notations cum poly prv finite =
in
(if poly && cum then
Inductiveops.infer_inductive_subtyping env_ar evd mind_ent
- else mind_ent), pl, impls
+ else mind_ent), Evd.universe_binders evd, impls
(* Very syntactical equality *)
let eq_local_binders bl1 bl2 =
@@ -1025,17 +1028,18 @@ let build_wellfounded (recname,pl,n,bl,arityc,body) poly r measure notation =
if List.length binders_rel > 1 then
let name = add_suffix recname "_func" in
let hook l gr _ =
- 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 pl, univs = Evd.universe_context ~names:pl ~extensible:plext !evdref in
- (*FIXME poly? *)
- let ce = definition_entry ~poly ~types:ty ~univs (EConstr.to_constr !evdref body) in
- (** FIXME: include locality *)
- let c = Declare.declare_constant recname (DefinitionEntry ce, IsDefinition Definition) in
- let gr = ConstRef c in
- if Impargs.is_implicit_args () || not (List.is_empty impls) then
- Impargs.declare_manual_implicits false gr [impls]
+ 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
+ (*FIXME poly? *)
+ let ce = definition_entry ~poly ~types:ty ~univs (EConstr.to_constr !evdref body) in
+ (** FIXME: include locality *)
+ let c = Declare.declare_constant recname (DefinitionEntry ce, IsDefinition Definition) in
+ let gr = ConstRef c in
+ let () = Universes.register_universe_binders gr (Evd.universe_binders !evdref) in
+ if Impargs.is_implicit_args () || not (List.is_empty impls) then
+ Impargs.declare_manual_implicits false gr [impls]
in
let typ = it_mkProd_or_LetIn top_arity binders in
hook, name, typ
@@ -1168,7 +1172,8 @@ let declare_fixpoint local poly ((fixnames,fixdefs,fixtypes),pl,ctx,fiximps) ind
List.map_i (fun i _ -> mkFix ((indexes,i),fixdecls)) 0 fixnames in
let evd = Evd.from_ctx ctx in
let evd = Evd.restrict_universe_context evd vars in
- let pl, ctx = Evd.check_univ_decl evd pl in
+ let ctx = Evd.check_univ_decl evd pl in
+ let pl = Evd.universe_binders evd in
let fixdecls = List.map Safe_typing.mk_pure_proof fixdecls in
ignore (List.map4 (DeclareDef.declare_fix (local, poly, Fixpoint) pl ctx)
fixnames fixdecls fixtypes fiximps);
@@ -1200,7 +1205,8 @@ let declare_cofixpoint local poly ((fixnames,fixdefs,fixtypes),pl,ctx,fiximps) n
let fiximps = List.map (fun (len,imps,idx) -> imps) fiximps in
let evd = Evd.from_ctx ctx in
let evd = Evd.restrict_universe_context evd vars in
- let pl, ctx = Evd.check_univ_decl evd pl in
+ let ctx = Evd.check_univ_decl evd pl in
+ let pl = Evd.universe_binders evd in
ignore (List.map4 (DeclareDef.declare_fix (local, poly, CoFixpoint) pl ctx)
fixnames fixdecls fixtypes fiximps);
(* Declare the recursive definitions *)
diff --git a/vernac/indschemes.ml b/vernac/indschemes.ml
index c0ddc7e2c..58f39e303 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.universe_context ~names:[] ~extensible:true 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 a025bfff8..cd30c7a68 100644
--- a/vernac/lemmas.ml
+++ b/vernac/lemmas.ml
@@ -49,7 +49,7 @@ 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
+ let uctx = UState.universe_context ~names:[] ~extensible:true 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)
@@ -223,7 +223,7 @@ let compute_proof_name locality = function
let avoid = Id.Set.of_list (Proof_global.get_all_proof_names ()) in
next_global_ident_away default_thm_id avoid
-let save_remaining_recthms (locality,p,kind) norm ctx binders body opaq i (id,(t_i,(_,imps))) =
+let save_remaining_recthms (locality,p,kind) norm ctx body opaq i (id,(t_i,(_,imps))) =
let t_i = norm t_i in
match body with
| None ->
@@ -420,9 +420,9 @@ 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 binders, ctx = Evd.check_univ_decl (Evd.from_ctx ctx) decl in
+ let ctx = Evd.check_univ_decl (Evd.from_ctx ctx) decl in
let body = Option.map norm body in
- List.map_i (save_remaining_recthms kind norm ctx binders body opaq) 1 other_thms 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) ->
maybe_declare_manual_implicits false ref imps;
@@ -513,9 +513,9 @@ let save_proof ?proof = function
| _ -> None in
let decl = Proof_global.get_universe_decl () in
let evd = Evd.from_ctx universes in
- let binders, ctx = Evd.check_univ_decl evd decl in
+ let ctx = Evd.check_univ_decl evd decl in
let poly = pi2 k in
- let binders = if poly then Some binders else None in
+ let binders = if poly then Some (UState.universe_binders universes) else None in
Admitted(id,k,(sec_vars, poly, (typ, ctx), None),
(universes, binders))
in
diff --git a/vernac/obligations.ml b/vernac/obligations.ml
index 590332d08..216801811 100644
--- a/vernac/obligations.ml
+++ b/vernac/obligations.ml
@@ -475,20 +475,17 @@ let declare_definition prg =
(Evd.evar_universe_context_subst prg.prg_ctx) in
let opaque = prg.prg_opaque in
let fix_exn = Hook.get get_fix_exn () in
- let pl, ctx = Evd.check_univ_decl (Evd.from_ctx prg.prg_ctx) prg.prg_univdecl in
+ let () = ignore(UState.check_univ_decl prg.prg_ctx prg.prg_univdecl) in
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)
in
let () = progmap_remove prg in
- let cst =
- DeclareDef.declare_definition prg.prg_name
- prg.prg_kind ce Universes.empty_binders prg.prg_implicits
- (Lemmas.mk_hook (fun l r -> Lemmas.call_hook fix_exn prg.prg_hook l r prg.prg_ctx; r))
- in
- Universes.register_universe_binders cst pl;
- cst
+ let ubinders = UState.universe_binders prg.prg_ctx in
+ DeclareDef.declare_definition prg.prg_name
+ prg.prg_kind ce ubinders prg.prg_implicits
+ (Lemmas.mk_hook (fun l r -> Lemmas.call_hook fix_exn prg.prg_hook l r prg.prg_ctx; r))
let rec lam_index n t acc =
match Constr.kind t with
@@ -893,7 +890,7 @@ 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
+ let uctx = UState.universe_context ~names:[] ~extensible:true ctx' in
Univ.UContext.instance uctx, ctx'
in
let obl = { obl with obl_body = Some (DefinedObl (cst, inst)) } in
diff --git a/vernac/record.ml b/vernac/record.ml
index 6ffbd1584..9fef8f682 100644
--- a/vernac/record.ml
+++ b/vernac/record.ml
@@ -168,9 +168,10 @@ let typecheck_params_and_fields finite def id pl t ps nots fs =
let typ = EConstr.to_constr evars typ in
let ce t = Pretyping.check_evars env0 Evd.empty evars (EConstr.of_constr t) in
let univs = Evd.check_univ_decl evars decl in
+ let ubinders = Evd.universe_binders evars in
List.iter (iter_constr ce) (List.rev newps);
List.iter (iter_constr ce) (List.rev newfs);
- univs, typ, template, imps, newps, impls, newfs
+ ubinders, univs, typ, template, imps, newps, impls, newfs
let degenerate_decl decl =
let id = match RelDecl.get_name decl with
@@ -605,7 +606,7 @@ let definition_structure (kind,cum,poly,finite,(is_coe,((loc,idstruc),pl)),ps,cf
if isnot_class && List.exists (fun opt -> not (Option.is_empty opt)) priorities then
user_err Pp.(str "Priorities only allowed for type class substructures");
(* Now, younger decl in params and fields is on top *)
- let (pl, ctx), arity, template, implpars, params, implfs, fields =
+ let pl, ctx, arity, template, implpars, params, implfs, fields =
States.with_state_protection (fun () ->
typecheck_params_and_fields finite (kind = Class true) idstruc pl s ps notations fs) () in
let sign = structure_signature (fields@params) in
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 62c7edb19..e2f28a371 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -1555,8 +1555,8 @@ let vernac_check_may_eval ?loc redexp glopt rc =
let sigma' = Evarconv.solve_unif_constraints_with_heuristics env sigma' in
Evarconv.check_problems_are_solved env sigma';
let sigma',nf = Evarutil.nf_evars_and_universes sigma' in
- let pl, uctx = Evd.universe_context ~names:[] ~extensible:true sigma' in
- let env = Environ.push_context uctx (Evarutil.nf_env_evar sigma' env) in
+ let uctx = Evd.universe_context_set sigma' in
+ let env = Environ.push_context_set uctx (Evarutil.nf_env_evar sigma' env) in
let c = nf c in
let j =
if Evarutil.has_undefined_evars sigma' (EConstr.of_constr c) then
@@ -1572,7 +1572,7 @@ let vernac_check_may_eval ?loc redexp glopt rc =
let j = { j with Environ.uj_type = Reductionops.nf_betaiota sigma' j.Environ.uj_type } in
Feedback.msg_notice (print_judgment env sigma' j ++
pr_ne_evar_set (fnl () ++ str "where" ++ fnl ()) (mt ()) sigma' l ++
- Printer.pr_universe_ctx sigma uctx)
+ Printer.pr_universe_ctx_set sigma uctx)
| Some r ->
let (sigma',r_interp) = Hook.get f_interp_redexp env sigma' r in
let redfun env evm c =
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-20 21:38:01 +0000