aboutsummaryrefslogtreecommitdiffhomepage
path: root/vernac
diff options
context:
space:
mode:
Diffstat (limited to 'vernac')
-rw-r--r--vernac/classes.ml4
-rw-r--r--vernac/command.ml44
-rw-r--r--vernac/command.mli2
-rw-r--r--vernac/declareDef.ml3
-rw-r--r--vernac/lemmas.ml35
-rw-r--r--vernac/obligations.ml2
-rw-r--r--vernac/record.ml5
7 files changed, 47 insertions, 48 deletions
diff --git a/vernac/classes.ml b/vernac/classes.ml
index b80741269..cb1d2f7c7 100644
--- a/vernac/classes.ml
+++ b/vernac/classes.ml
@@ -126,7 +126,7 @@ let declare_instance_constant k info global imps ?hook id decl poly evm term ter
let cdecl = (DefinitionEntry entry, kind) in
let kn = Declare.declare_constant id cdecl in
Declare.definition_message id;
- Universes.register_universe_binders (ConstRef kn) (Evd.universe_binders evm);
+ Declare.declare_univ_binders (ConstRef kn) (Evd.universe_binders evm);
instance_hook k info global imps ?hook (ConstRef kn);
id
@@ -208,7 +208,7 @@ let new_instance ?(abstract=false) ?(global=false) ?(refine= !refine_instance)
(ParameterEntry
(None,(termtype,univs),None), Decl_kinds.IsAssumption Decl_kinds.Logical)
in
- Universes.register_universe_binders (ConstRef cst) (Evd.universe_binders !evars);
+ Declare.declare_univ_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 01c7f149b..66d4fe984 100644
--- a/vernac/command.ml
+++ b/vernac/command.ml
@@ -95,7 +95,7 @@ let interp_definition pl bl poly red_option c ctypopt =
let impls, ((env_bl, ctx), imps1) = interp_context_evars env evdref bl in
let ctx = List.map (fun d -> map_rel_decl EConstr.Unsafe.to_constr d) ctx in
let nb_args = Context.Rel.nhyps ctx in
- let imps,pl,ce =
+ let imps,ce =
match ctypopt with
None ->
let subst = evd_comb0 Evd.nf_univ_variables evdref in
@@ -105,11 +105,10 @@ let interp_definition pl bl poly red_option c ctypopt =
let c = EConstr.Unsafe.to_constr c in
let nf,subst = Evarutil.e_nf_evars_and_universes evdref in
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 uctx = Evd.check_univ_decl ~poly evd decl in
- let binders = Evd.universe_binders evd in
- imps1@(Impargs.lift_implicits nb_args imps2), binders,
+ let vars = EConstr.universes_of_constr !evdref (EConstr.of_constr body) in
+ let () = evdref := Evd.restrict_universe_context !evdref vars in
+ let uctx = Evd.check_univ_decl ~poly !evdref decl in
+ imps1@(Impargs.lift_implicits nb_args imps2),
definition_entry ~univs:uctx body
| Some ctyp ->
let ty, impsty = interp_type_evars_impls ~impls env_bl evdref ctyp in
@@ -131,23 +130,22 @@ let interp_definition pl bl poly red_option c ctypopt =
in
if not (try List.for_all chk imps2 with Not_found -> false)
then warn_implicits_in_term ();
- 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 uctx = Evd.check_univ_decl ~poly ctx decl in
- let binders = Evd.universe_binders evd in
- imps1@(Impargs.lift_implicits nb_args impsty), binders,
- definition_entry ~types:typ
- ~univs:uctx body
+ let bodyvars = EConstr.universes_of_constr !evdref (EConstr.of_constr body) in
+ let tyvars = EConstr.universes_of_constr !evdref (EConstr.of_constr ty) in
+ let vars = Univ.LSet.union bodyvars tyvars in
+ let () = evdref := Evd.restrict_universe_context !evdref vars in
+ let uctx = Evd.check_univ_decl ~poly !evdref decl in
+ imps1@(Impargs.lift_implicits nb_args impsty),
+ definition_entry ~types:typ ~univs:uctx body
in
- red_constant_entry (Context.Rel.length ctx) ce !evdref red_option, !evdref, decl, pl, imps
+ (red_constant_entry (Context.Rel.length ctx) ce !evdref red_option, !evdref, decl, imps)
-let check_definition (ce, evd, _, _, imps) =
+let check_definition (ce, evd, _, imps) =
check_evars_are_solved (Global.env ()) evd Evd.empty;
ce
let do_definition ident k univdecl bl red_option c ctypopt hook =
- let (ce, evd, univdecl, pl', imps as def) =
+ let (ce, evd, univdecl, imps as def) =
interp_definition univdecl bl (pi2 k) red_option c ctypopt
in
if Flags.is_program_mode () then
@@ -168,7 +166,7 @@ let do_definition ident k univdecl bl red_option c ctypopt hook =
ignore(Obligations.add_definition
ident ~term:c cty ctx ~univdecl ~implicits:imps ~kind:k ~hook obls)
else let ce = check_definition def in
- ignore(DeclareDef.declare_definition ident k ce pl' imps
+ ignore(DeclareDef.declare_definition ident k ce (Evd.universe_binders evd) imps
(Lemmas.mk_hook
(fun l r -> Lemmas.call_hook (fun exn -> exn) hook l r;r)))
@@ -224,7 +222,7 @@ match local with
let kn = declare_constant ident ~local decl in
let gr = ConstRef kn in
let () = maybe_declare_manual_implicits false gr imps in
- let () = Universes.register_universe_binders gr pl in
+ let () = Declare.declare_univ_binders gr pl in
let () = assumption_message ident in
let () = if do_instance then Typeclasses.declare_instance None false gr in
let () = if is_coe then Class.try_add_new_coercion gr ~local p in
@@ -712,7 +710,7 @@ let declare_mutual_inductive_with_eliminations mie pl impls =
let ind = (mind,i) in
let gr = IndRef ind in
maybe_declare_manual_implicits false gr indimpls;
- Universes.register_universe_binders gr pl;
+ Declare.declare_univ_binders gr pl;
List.iteri
(fun j impls ->
maybe_declare_manual_implicits false
@@ -1268,7 +1266,7 @@ let collect_evars_of_term evd c ty =
Evar.Set.fold (fun ev acc -> Evd.add acc ev (Evd.find_undefined evd ev))
evars (Evd.from_ctx (Evd.evar_universe_context evd))
-let do_program_recursive local p fixkind fixl ntns =
+let do_program_recursive local poly fixkind fixl ntns =
let isfix = fixkind != Obligations.IsCoFixpoint in
let (env, rec_sign, pl, evd), fix, info =
interp_recursive isfix fixl ntns
@@ -1310,8 +1308,8 @@ let do_program_recursive local p fixkind fixl ntns =
end in
let ctx = Evd.evar_universe_context evd in
let kind = match fixkind with
- | Obligations.IsFixpoint _ -> (local, p, Fixpoint)
- | Obligations.IsCoFixpoint -> (local, p, CoFixpoint)
+ | Obligations.IsFixpoint _ -> (local, poly, Fixpoint)
+ | Obligations.IsCoFixpoint -> (local, poly, CoFixpoint)
in
Obligations.add_mutual_definitions defs ~kind ~univdecl:pl ctx ntns fixkind
diff --git a/vernac/command.mli b/vernac/command.mli
index 070f3e112..a1f916c78 100644
--- a/vernac/command.mli
+++ b/vernac/command.mli
@@ -28,7 +28,7 @@ val do_constraint : polymorphic ->
val interp_definition :
Vernacexpr.universe_decl_expr option -> local_binder_expr list -> polymorphic -> red_expr option -> constr_expr ->
constr_expr option -> Safe_typing.private_constants definition_entry * Evd.evar_map *
- Univdecls.universe_decl * Universes.universe_binders * Impargs.manual_implicits
+ Univdecls.universe_decl * Impargs.manual_implicits
val do_definition : Id.t -> definition_kind -> Vernacexpr.universe_decl_expr option ->
local_binder_expr list -> red_expr option -> constr_expr ->
diff --git a/vernac/declareDef.ml b/vernac/declareDef.ml
index 980db4109..dfac78c04 100644
--- a/vernac/declareDef.ml
+++ b/vernac/declareDef.ml
@@ -36,7 +36,7 @@ let declare_global_definition ident ce local k pl imps =
let kn = declare_constant ident ~local (DefinitionEntry ce, IsDefinition k) in
let gr = ConstRef kn in
let () = maybe_declare_manual_implicits false gr imps in
- let () = Universes.register_universe_binders gr pl in
+ let () = Declare.declare_univ_binders gr pl in
let () = definition_message ident in
gr
@@ -49,6 +49,7 @@ let declare_definition ident (local, p, k) ce pl imps hook =
let () = definition_message ident in
let gr = VarRef ident in
let () = maybe_declare_manual_implicits false gr imps in
+ let () = Declare.declare_univ_binders gr pl in
let () = if Proof_global.there_are_pending_proofs () then
warn_definition_not_visible ident
in
diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml
index 42631a15b..200c2260e 100644
--- a/vernac/lemmas.ml
+++ b/vernac/lemmas.ml
@@ -177,7 +177,7 @@ let look_for_possibly_mutual_statements = function
(* Saving a goal *)
-let save ?export_seff id const cstrs pl do_guard (locality,poly,kind) hook =
+let save ?export_seff id const uctx do_guard (locality,poly,kind) hook =
let fix_exn = Future.fix_exn_of const.Entries.const_entry_body in
try
let const = adjust_guardness_conditions const do_guard in
@@ -204,7 +204,7 @@ let save ?export_seff id const cstrs pl do_guard (locality,poly,kind) hook =
(locality, ConstRef kn)
in
definition_message id;
- Universes.register_universe_binders r (Option.default Universes.empty_binders pl);
+ Declare.declare_univ_binders r (UState.universe_binders uctx);
call_hook (fun exn -> exn) hook l r
with e when CErrors.noncritical e ->
let e = CErrors.push e in
@@ -286,17 +286,17 @@ let save_hook = ref ignore
let set_save_hook f = save_hook := f
let save_named ?export_seff proof =
- let id,const,(cstrs,pl),do_guard,persistence,hook = proof in
- save ?export_seff id const cstrs pl do_guard persistence hook
+ let id,const,uctx,do_guard,persistence,hook = proof in
+ save ?export_seff id const uctx do_guard persistence hook
let check_anonymity id save_ident =
if not (String.equal (atompart_of_id id) (Id.to_string (default_thm_id))) then
user_err Pp.(str "This command can only be used for unnamed theorem.")
let save_anonymous ?export_seff proof save_ident =
- let id,const,(cstrs,pl),do_guard,persistence,hook = proof in
+ let id,const,uctx,do_guard,persistence,hook = proof in
check_anonymity id save_ident;
- save ?export_seff save_ident const cstrs pl do_guard persistence hook
+ save ?export_seff save_ident const uctx do_guard persistence hook
(* Admitted *)
@@ -312,7 +312,7 @@ let admit (id,k,e) pl hook () =
| Local, _, _ | Discharge, _, _ -> warn_let_as_axiom id
in
let () = assumption_message id in
- Universes.register_universe_binders (ConstRef kn) (Option.default Universes.empty_binders pl);
+ Declare.declare_univ_binders (ConstRef kn) pl;
call_hook (fun exn -> exn) hook Global (ConstRef kn)
(* Starting a goal *)
@@ -330,8 +330,8 @@ let get_proof proof do_guard hook opacity =
let universe_proof_terminator compute_guard hook =
let open Proof_global in
make_terminator begin function
- | Admitted (id,k,pe,(ctx,pl)) ->
- admit (id,k,pe) pl (hook (Some ctx)) ();
+ | Admitted (id,k,pe,ctx) ->
+ admit (id,k,pe) (UState.universe_binders ctx) (hook (Some ctx)) ();
Feedback.feedback Feedback.AddedAxiom
| Proved (opaque,idopt,proof) ->
let is_opaque, export_seff = match opaque with
@@ -339,7 +339,7 @@ let universe_proof_terminator compute_guard hook =
| Vernacexpr.Opaque -> true, false
in
let proof = get_proof proof compute_guard
- (hook (Some (fst proof.Proof_global.universes))) is_opaque in
+ (hook (Some (proof.Proof_global.universes))) is_opaque in
begin match idopt with
| None -> save_named ~export_seff proof
| Some (_,id) -> save_anonymous ~export_seff proof id
@@ -417,7 +417,7 @@ let start_proof_with_initialization kind ctx decl recguard thms snl hook =
| (id,(t,(_,imps)))::other_thms ->
let hook ctx strength ref =
let ctx = match ctx with
- | None -> Evd.empty_evar_universe_context
+ | None -> UState.empty
| Some ctx -> ctx
in
let other_thms_data =
@@ -426,9 +426,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 ctx = UState.check_univ_decl ~poly:(pi2 kind) 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 uctx = UState.check_univ_decl ~poly:(pi2 kind) ctx decl in
+ List.map_i (save_remaining_recthms kind norm uctx 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;
@@ -496,7 +496,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 = UState.const_univ_entry ~poly:(pi2 k) (fst universes) in
+ let ctx = UState.const_univ_entry ~poly:(pi2 k) universes in
let sec_vars = if !keep_admitted_vars then const_entry_secctx else None in
Admitted(id, k, (sec_vars, (typ, ctx), None), universes)
| None ->
@@ -518,12 +518,9 @@ let save_proof ?proof = function
Some (Environ.keep_hyps env (Id.Set.union ids_typ ids_def))
| _ -> None in
let decl = Proof_global.get_universe_decl () in
- let evd = Evd.from_ctx universes in
let poly = pi2 k in
- let ctx = Evd.check_univ_decl ~poly evd decl in
- let binders = if poly then Some (UState.universe_binders universes) else None in
- Admitted(id,k,(sec_vars, (typ, ctx), None),
- (universes, binders))
+ let ctx = UState.check_univ_decl ~poly universes decl in
+ Admitted(id,k,(sec_vars, (typ, ctx), None), universes)
in
Proof_global.apply_terminator (Proof_global.get_terminator ()) pe
| Vernacexpr.Proved (is_opaque,idopt) ->
diff --git a/vernac/obligations.ml b/vernac/obligations.ml
index 1046d68f8..24d664951 100644
--- a/vernac/obligations.ml
+++ b/vernac/obligations.ml
@@ -833,7 +833,7 @@ let obligation_terminator name num guard hook auto pf =
let entry = Safe_typing.inline_private_constants_in_definition_entry env entry in
let ty = entry.Entries.const_entry_type in
let (body, cstr), () = Future.force entry.Entries.const_entry_body in
- let sigma = Evd.from_ctx (fst uctx) in
+ let sigma = Evd.from_ctx uctx in
let sigma = Evd.merge_context_set ~sideff:true Evd.univ_rigid sigma cstr in
Inductiveops.control_only_guard (Global.env ()) body;
(** Declare the obligation ourselves and drop the hook *)
diff --git a/vernac/record.ml b/vernac/record.ml
index 1d255b08e..1cdc538b5 100644
--- a/vernac/record.ml
+++ b/vernac/record.ml
@@ -613,7 +613,7 @@ let definition_structure (kind,cum,poly,finite,(is_coe,((loc,idstruc),pl)),ps,cf
States.with_state_protection (fun () ->
typecheck_params_and_fields finite (kind = Class true) idstruc poly pl s ps notations fs) () in
let sign = structure_signature (fields@params) in
- match kind with
+ let gr = match kind with
| Class def ->
let priorities = List.map (fun id -> {hint_priority = id; hint_pattern = None}) priorities in
let gr = declare_class finite def cum pl univs (loc,idstruc) idbuild
@@ -638,3 +638,6 @@ let definition_structure (kind,cum,poly,finite,(is_coe,((loc,idstruc),pl)),ps,cf
idbuild implpars params arity template implfs
fields is_coe (List.map (fun coe -> not (Option.is_empty coe)) coers) sign in
IndRef ind
+ in
+ Declare.declare_univ_binders gr pl;
+ gr
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-12 22:51:07 +0000