aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--plugins/funind/gen_principle.ml1
-rw-r--r--vernac/classes.ml23
-rw-r--r--vernac/comAssumption.ml2
-rw-r--r--vernac/declareDef.ml11
-rw-r--r--vernac/declareDef.mli15
-rw-r--r--vernac/declareObl.ml29
-rw-r--r--vernac/lemmas.ml1
7 files changed, 47 insertions, 35 deletions
diff --git a/plugins/funind/gen_principle.ml b/plugins/funind/gen_principle.ml
index 4242da2802..47e56b81aa 100644
--- a/plugins/funind/gen_principle.ml
+++ b/plugins/funind/gen_principle.ml
@@ -291,6 +291,7 @@ let generate_functional_principle (evd: Evd.evar_map ref)
*)
let uctx = Evd.evar_universe_context sigma in
let hook_data = hook, uctx, [] in
+ let entry = DeclareDef.ClosedDef.of_proof_entry entry in
let _ : Names.GlobRef.t = DeclareDef.declare_definition
~name:new_princ_name ~hook_data
~scope:(DeclareDef.Global Declare.ImportDefaultBehavior)
diff --git a/vernac/classes.ml b/vernac/classes.ml
index 65d20a13a1..88b6ab34ff 100644
--- a/vernac/classes.ml
+++ b/vernac/classes.ml
@@ -304,22 +304,21 @@ let id_of_class cl =
mip.(0).Declarations.mind_typename
| _ -> assert false
-let instance_hook info global imps ?hook cst =
- Impargs.maybe_declare_manual_implicits false cst imps;
+let instance_hook info global ?hook cst =
let info = intern_info info in
let env = Global.env () in
let sigma = Evd.from_env env in
declare_instance env sigma (Some info) (not global) cst;
(match hook with Some h -> h cst | None -> ())
-let declare_instance_constant info global imps ?hook name udecl poly sigma term termtype =
+let declare_instance_constant info global impargs ?hook name udecl poly sigma term termtype =
let kind = Decls.(IsDefinition Instance) in
let sigma, entry = DeclareDef.prepare_definition
~poly sigma ~udecl ~types:(Some termtype) ~body:term in
- let kn = Declare.declare_constant ~name ~kind (Declare.DefinitionEntry entry) in
- Declare.definition_message name;
- DeclareUniv.declare_univ_binders (GlobRef.ConstRef kn) (Evd.universe_binders sigma);
- instance_hook info global imps ?hook (GlobRef.ConstRef kn)
+ let ubind = Evd.universe_binders sigma in
+ let scope = DeclareDef.Global Declare.ImportDefaultBehavior in
+ let kn = DeclareDef.declare_definition ~name ~kind ~scope ~ubind ~impargs entry in
+ instance_hook info global ?hook kn
let do_declare_instance sigma ~global ~poly k u ctx ctx' pri udecl impargs subst name =
let subst = List.fold_left2
@@ -332,7 +331,9 @@ let do_declare_instance sigma ~global ~poly k u ctx ctx' pri udecl impargs subst
let cst = Declare.declare_constant ~name
~kind:Decls.(IsAssumption Logical) (Declare.ParameterEntry entry) in
DeclareUniv.declare_univ_binders (GlobRef.ConstRef cst) (Evd.universe_binders sigma);
- instance_hook pri global impargs (GlobRef.ConstRef cst)
+ let cst = (GlobRef.ConstRef cst) in
+ Impargs.maybe_declare_manual_implicits false cst impargs;
+ instance_hook pri global cst
let declare_instance_program env sigma ~global ~poly name pri imps udecl term termtype =
let hook { DeclareDef.Hook.S.scope; dref; _ } =
@@ -351,7 +352,7 @@ let declare_instance_program env sigma ~global ~poly name pri imps udecl term te
Obligations.add_definition ~name ~term ~udecl ~scope ~poly ~kind ~hook typ ~uctx obls
in ()
-let declare_instance_open sigma ?hook ~tac ~global ~poly id pri imps udecl ids term termtype =
+let declare_instance_open sigma ?hook ~tac ~global ~poly id pri impargs udecl ids term termtype =
(* spiwack: it is hard to reorder the actions to do
the pretyping after the proof has opened. As a
consequence, we use the low-level primitives to code
@@ -359,12 +360,12 @@ let declare_instance_open sigma ?hook ~tac ~global ~poly id pri imps udecl ids t
let gls = List.rev (Evd.future_goals sigma) in
let sigma = Evd.reset_future_goals sigma in
let kind = Decls.(IsDefinition Instance) in
- let hook = DeclareDef.Hook.(make (fun { S.dref ; _ } -> instance_hook pri global imps ?hook dref)) in
+ let hook = DeclareDef.Hook.(make (fun { S.dref ; _ } -> instance_hook pri global ?hook dref)) in
let info = Lemmas.Info.make ~hook ~kind () in
(* XXX: We need to normalize the type, otherwise Admitted / Qed will fails!
This is due to a bug in proof_global :( *)
let termtype = Evarutil.nf_evar sigma termtype in
- let lemma = Lemmas.start_lemma ~name:id ~poly ~udecl ~info sigma termtype in
+ let lemma = Lemmas.start_lemma ~name:id ~poly ~udecl ~info ~impargs sigma termtype in
(* spiwack: I don't know what to do with the status here. *)
let lemma =
match term with
diff --git a/vernac/comAssumption.ml b/vernac/comAssumption.ml
index dc9c8e2d3c..cb9acda770 100644
--- a/vernac/comAssumption.ml
+++ b/vernac/comAssumption.ml
@@ -203,6 +203,8 @@ let context_insection sigma ~poly ctx =
else Monomorphic_entry Univ.ContextSet.empty
in
let entry = Declare.definition_entry ~univs ~types:t b in
+ (* XXX Fixme: Use DeclareDef.prepare_definition *)
+ let entry = DeclareDef.ClosedDef.of_proof_entry entry in
let _ : GlobRef.t = DeclareDef.declare_definition ~name ~scope:DeclareDef.Discharge
~kind:Decls.(IsDefinition Definition) ~ubind:UnivNames.empty_binders ~impargs:[] entry
in
diff --git a/vernac/declareDef.ml b/vernac/declareDef.ml
index 2528dfd38f..84310cba65 100644
--- a/vernac/declareDef.ml
+++ b/vernac/declareDef.ml
@@ -38,6 +38,13 @@ module Hook = struct
end
+module ClosedDef = struct
+
+ type t = Evd.side_effects Declare.proof_entry
+
+ let of_proof_entry x = x
+end
+
(* Locality stuff *)
let declare_definition ~name ~scope ~kind ?hook_data ~ubind ~impargs ce =
let should_suggest = ce.Declare.proof_entry_opaque &&
@@ -153,14 +160,14 @@ let declare_assumption ?fix_exn ~name ~scope ~hook ~impargs ~uctx pe =
(* Preparing proof entries *)
-let prepare_definition ?opaque ?inline ~poly ~udecl ~types ~body sigma =
+let prepare_definition ?opaque ?inline ?fix_exn ~poly ~udecl ~types ~body sigma =
let env = Global.env () in
Pretyping.check_evars_are_solved ~program_mode:false env sigma;
let sigma, (body, types) = Evarutil.finalize ~abort_on_undefined_evars:true
sigma (fun nf -> nf body, Option.map nf types)
in
let univs = Evd.check_univ_decl ~poly sigma udecl in
- sigma, definition_entry ?opaque ?inline ?types ~univs body
+ sigma, definition_entry ?fix_exn ?opaque ?inline ?types ~univs body
let prepare_obligation ?opaque ?inline ~name ~poly ~udecl ~types ~body sigma =
let sigma, (body, types) = Evarutil.finalize ~abort_on_undefined_evars:false
diff --git a/vernac/declareDef.mli b/vernac/declareDef.mli
index f72954d8c2..9c5cd6fc2a 100644
--- a/vernac/declareDef.mli
+++ b/vernac/declareDef.mli
@@ -39,6 +39,13 @@ module Hook : sig
val call : ?hook:t -> S.t -> unit
end
+module ClosedDef : sig
+ type t
+
+ (* Don't use for non-interactive proofs *)
+ val of_proof_entry : Evd.side_effects Declare.proof_entry -> t
+end
+
val declare_definition
: name:Id.t
-> scope:locality
@@ -46,7 +53,7 @@ val declare_definition
-> ?hook_data:(Hook.t * UState.t * (Id.t * Constr.t) list)
-> ubind:UnivNames.universe_binders
-> impargs:Impargs.manual_implicits
- -> Evd.side_effects Declare.proof_entry
+ -> ClosedDef.t
-> GlobRef.t
val declare_assumption
@@ -88,15 +95,19 @@ val declare_mutually_recursive
-> Recthm.t list
-> Names.GlobRef.t list
+(* The common use of the returned evar_map is to obtain the universe
+ binders and context for the hook; we should refactor that soon by
+ merging prepare and declare. *)
val prepare_definition
: ?opaque:bool
-> ?inline:bool
+ -> ?fix_exn:(Exninfo.iexn -> Exninfo.iexn)
-> poly:bool
-> udecl:UState.universe_decl
-> types:EConstr.t option
-> body:EConstr.t
-> Evd.evar_map
- -> Evd.evar_map * Evd.side_effects Declare.proof_entry
+ -> Evd.evar_map * ClosedDef.t
val prepare_obligation
: ?opaque:bool
diff --git a/vernac/declareObl.ml b/vernac/declareObl.ml
index 24a52eaca4..e643ffa98d 100644
--- a/vernac/declareObl.ml
+++ b/vernac/declareObl.ml
@@ -362,28 +362,17 @@ let get_fix_exn, stm_get_fix_exn = Hook.make ()
let declare_definition prg =
let varsubst = obligation_substitution true prg in
- let body, typ = subst_prog varsubst prg in
- let nf =
- UnivSubst.nf_evars_and_universes_opt_subst
- (fun x -> None)
- (UState.subst prg.prg_ctx)
- in
- let opaque = prg.prg_opaque in
+ let sigma = Evd.from_ctx prg.prg_ctx in
+ let body, types = subst_prog varsubst prg in
+ let body, types = EConstr.(of_constr body, Some (of_constr types)) in
+ let opaque, poly, udecl = prg.prg_opaque, prg.prg_poly, prg.prg_univdecl in
let fix_exn = Hook.get get_fix_exn () in
- let typ = nf typ in
- let body = nf body in
- let obls = List.map (fun (id, (_, c)) -> (id, nf c)) varsubst in
- let uvars =
- Univ.LSet.union
- (Vars.universes_of_constr typ)
- (Vars.universes_of_constr body)
- in
- let uctx = UState.restrict prg.prg_ctx uvars in
- let univs =
- UState.check_univ_decl ~poly:prg.prg_poly uctx prg.prg_univdecl
- in
- let ce = Declare.definition_entry ~fix_exn ~opaque ~types:typ ~univs body in
+ let obls = List.map (fun (id, (_, c)) -> (id, c)) varsubst in
+ (* XXX: This is doing normalization twice *)
+ let sigma, ce =
+ DeclareDef.prepare_definition ~fix_exn ~opaque ~poly ~udecl ~types ~body sigma in
let () = progmap_remove prg in
+ let uctx = Evd.evar_universe_context sigma in
let ubind = UState.universe_binders uctx in
let hook_data = Option.map (fun hook -> hook, uctx, obls) prg.prg_hook in
DeclareDef.declare_definition
diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml
index e4a625d65c..a1bcf95bf5 100644
--- a/vernac/lemmas.ml
+++ b/vernac/lemmas.ml
@@ -242,6 +242,7 @@ end = struct
Declare.Internal.map_entry_body pe
~f:(fun ((body, ctx), eff) -> (select_body i body, ctx), eff)
in
+ let pe = DeclareDef.ClosedDef.of_proof_entry pe in
DeclareDef.declare_definition ~name ~scope ~kind ?hook_data ~ubind ~impargs pe
let declare_mutdef ~info ~uctx const =
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 14:51:25 +0000