aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--doc/plugin_tutorial/tuto1/src/simple_declare.ml5
-rw-r--r--plugins/funind/gen_principle.ml5
-rw-r--r--vernac/classes.ml5
-rw-r--r--vernac/comAssumption.ml7
-rw-r--r--vernac/comDefinition.ml4
-rw-r--r--vernac/declareDef.ml28
-rw-r--r--vernac/declareDef.mli47
-rw-r--r--vernac/declareObl.ml7
-rw-r--r--vernac/lemmas.ml3
9 files changed, 55 insertions, 56 deletions
diff --git a/doc/plugin_tutorial/tuto1/src/simple_declare.ml b/doc/plugin_tutorial/tuto1/src/simple_declare.ml
index a2783d80e8..8c4dc0e8a6 100644
--- a/doc/plugin_tutorial/tuto1/src/simple_declare.ml
+++ b/doc/plugin_tutorial/tuto1/src/simple_declare.ml
@@ -1,7 +1,6 @@
let edeclare ?hook ~name ~poly ~scope ~kind ~opaque ~udecl ~impargs sigma body tyopt =
- let ce = DeclareDef.prepare_definition
- ~opaque ~poly sigma ~udecl ~types:tyopt ~body in
- DeclareDef.declare_definition ~name ~scope ~kind ~impargs ?hook ce
+ DeclareDef.declare_definition ~name ~scope ~kind ~impargs ?hook
+ ~opaque ~poly ~udecl ~types:tyopt ~body sigma
let declare_definition ~poly name sigma body =
let udecl = UState.default_univ_decl in
diff --git a/plugins/funind/gen_principle.ml b/plugins/funind/gen_principle.ml
index ebd280ecf6..45c46c56f4 100644
--- a/plugins/funind/gen_principle.ml
+++ b/plugins/funind/gen_principle.ml
@@ -290,13 +290,12 @@ let generate_functional_principle (evd: Evd.evar_map ref)
Don't forget to close the goal if an error is raised !!!!
*)
let uctx = Evd.evar_universe_context sigma in
- let entry = DeclareDef.ClosedDef.of_proof_entry ~uctx entry in
- let _ : Names.GlobRef.t = DeclareDef.declare_definition
+ let _ : Names.GlobRef.t = DeclareDef.declare_entry
~name:new_princ_name ~hook
~scope:(DeclareDef.Global Declare.ImportDefaultBehavior)
~kind:Decls.(IsProof Theorem)
~impargs:[]
- entry in
+ ~uctx entry in
()
with e when CErrors.noncritical e ->
raise (Defining_principle e)
diff --git a/vernac/classes.ml b/vernac/classes.ml
index 40c1a5d97d..6e929de581 100644
--- a/vernac/classes.ml
+++ b/vernac/classes.ml
@@ -313,10 +313,9 @@ let instance_hook info global ?hook cst =
let declare_instance_constant info global impargs ?hook name udecl poly sigma term termtype =
let kind = Decls.(IsDefinition Instance) in
- let entry = DeclareDef.prepare_definition
- ~poly sigma ~udecl ~types:(Some termtype) ~body:term in
let scope = DeclareDef.Global Declare.ImportDefaultBehavior in
- let kn = DeclareDef.declare_definition ~name ~kind ~scope ~impargs entry in
+ let kn = DeclareDef.declare_definition ~name ~kind ~scope ~impargs
+ ~opaque:false ~poly sigma ~udecl ~types:(Some termtype) ~body:term in
instance_hook info global ?hook kn
let do_declare_instance sigma ~global ~poly k u ctx ctx' pri udecl impargs subst name =
diff --git a/vernac/comAssumption.ml b/vernac/comAssumption.ml
index 4a82696ea6..47ae03e0a3 100644
--- a/vernac/comAssumption.ml
+++ b/vernac/comAssumption.ml
@@ -205,9 +205,10 @@ let context_insection sigma ~poly ctx =
let entry = Declare.definition_entry ~univs ~types:t b in
(* XXX Fixme: Use DeclareDef.prepare_definition *)
let uctx = Evd.evar_universe_context sigma in
- let entry = DeclareDef.ClosedDef.of_proof_entry ~uctx entry in
- let _ : GlobRef.t = DeclareDef.declare_definition ~name ~scope:DeclareDef.Discharge
- ~kind:Decls.(IsDefinition Definition) ~impargs:[] entry
+ let kind = Decls.(IsDefinition Definition) in
+ let _ : GlobRef.t =
+ DeclareDef.declare_entry ~name ~scope:DeclareDef.Discharge
+ ~kind ~impargs:[] ~uctx entry
in
()
in
diff --git a/vernac/comDefinition.ml b/vernac/comDefinition.ml
index bf4567e57f..3532d16315 100644
--- a/vernac/comDefinition.ml
+++ b/vernac/comDefinition.ml
@@ -74,10 +74,10 @@ let do_definition ?hook ~name ~scope ~poly ~kind udecl bl red_option c ctypopt =
let (body, types), evd, udecl, impargs =
interp_definition ~program_mode udecl bl ~poly red_option c ctypopt
in
- let ce = DeclareDef.prepare_definition ~opaque:false ~poly evd ~udecl ~types ~body in
let kind = Decls.IsDefinition kind in
let _ : Names.GlobRef.t =
- DeclareDef.declare_definition ~name ~scope ~kind ?hook ~impargs ce
+ DeclareDef.declare_definition ~name ~scope ~kind ?hook ~impargs
+ ~opaque:false ~poly evd ~udecl ~types ~body
in ()
let do_definition_program ?hook ~name ~scope ~poly ~kind udecl bl red_option c ctypopt =
diff --git a/vernac/declareDef.ml b/vernac/declareDef.ml
index 14d3daf453..356e8f091e 100644
--- a/vernac/declareDef.ml
+++ b/vernac/declareDef.ml
@@ -37,19 +37,8 @@ module Hook = struct
end
-module ClosedDef = struct
-
- type t =
- { entry : Evd.side_effects Declare.proof_entry
- ; uctx : UState.t
- }
-
- let of_proof_entry ~uctx entry = { entry; uctx }
-end
-
(* Locality stuff *)
-let declare_definition ~name ~scope ~kind ?hook ?(obls=[]) ~impargs ce =
- let { ClosedDef.entry; uctx } = ce in
+let declare_entry ~name ~scope ~kind ?hook ?(obls=[]) ~impargs ~uctx entry =
let should_suggest = entry.Declare.proof_entry_opaque &&
Option.is_empty entry.Declare.proof_entry_secctx in
let ubind = UState.universe_binders uctx in
@@ -70,9 +59,9 @@ let declare_definition ~name ~scope ~kind ?hook ?(obls=[]) ~impargs ce =
Option.iter (fun hook -> Hook.call ~hook { Hook.S.uctx; obls; scope; dref }) hook;
dref
-let declare_definition ~name ~scope ~kind ?hook ?obls ~impargs ce =
- let fix_exn = Declare.Internal.get_fix_exn ce.ClosedDef.entry in
- try declare_definition ~name ~scope ~kind ?hook ?obls ~impargs ce
+let declare_entry ~name ~scope ~kind ?hook ?obls ~impargs ~uctx entry =
+ let fix_exn = Declare.Internal.get_fix_exn entry in
+ try declare_entry ~name ~scope ~kind ?hook ?obls ~impargs ~uctx entry
with exn ->
let exn = Exninfo.capture exn in
Exninfo.iraise (fix_exn exn)
@@ -120,7 +109,7 @@ let declare_mutually_recursive ~opaque ~scope ~kind ~poly ~uctx ~udecl ~ntns ~re
let csts = CList.map2
(fun Recthm.{ name; typ; impargs } body ->
let entry = Declare.definition_entry ~opaque ~types:typ ~univs body in
- declare_definition ~name ~scope ~kind ~impargs { ClosedDef.entry; uctx })
+ declare_entry ~name ~scope ~kind ~impargs ~uctx entry)
fixitems fixdecls
in
let isfix = Option.is_empty possible_indexes in
@@ -167,7 +156,12 @@ let prepare_definition ?opaque ?inline ?fix_exn ~poly ~udecl ~types ~body sigma
let univs = Evd.check_univ_decl ~poly sigma udecl in
let entry = definition_entry ?fix_exn ?opaque ?inline ?types ~univs body in
let uctx = Evd.evar_universe_context sigma in
- { ClosedDef.entry; uctx }
+ entry, uctx
+
+let declare_definition ~name ~scope ~kind ~opaque ~impargs ~udecl ?hook
+ ?obls ~poly ?inline ~types ~body ?fix_exn sigma =
+ let entry, uctx = prepare_definition ?fix_exn ~opaque ~poly ~udecl ~types ~body ?inline sigma in
+ declare_entry ~name ~scope ~kind ~impargs ?obls ?hook ~uctx entry
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 8f3db59ba9..3bc1e25f19 100644
--- a/vernac/declareDef.mli
+++ b/vernac/declareDef.mli
@@ -39,23 +39,39 @@ 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
- : uctx:UState.t
- -> Evd.side_effects Declare.proof_entry -> t
-end
+(** Declare an interactively-defined constant *)
+val declare_entry
+ : name:Id.t
+ -> scope:locality
+ -> kind:Decls.logical_kind
+ -> ?hook:Hook.t
+ -> ?obls:(Id.t * Constr.t) list
+ -> impargs:Impargs.manual_implicits
+ -> uctx:UState.t
+ -> Evd.side_effects Declare.proof_entry
+ -> GlobRef.t
+(** Declares a non-interactive constant; [body] and [types] will be
+ normalized w.r.t. the passed [evar_map] [sigma]. Universes should
+ be handled properly, including minimization and restriction. Note
+ that [sigma] is checked for unresolved evars, thus you should be
+ careful not to submit open terms or evar maps with stale,
+ unresolved existentials *)
val declare_definition
: name:Id.t
-> scope:locality
-> kind:Decls.logical_kind
+ -> opaque:bool
+ -> impargs:Impargs.manual_implicits
+ -> udecl:UState.universe_decl
-> ?hook:Hook.t
-> ?obls:(Id.t * Constr.t) list
- -> impargs:Impargs.manual_implicits
- -> ClosedDef.t
+ -> poly:bool
+ -> ?inline:bool
+ -> types:EConstr.t option
+ -> body:EConstr.t
+ -> ?fix_exn:(Exninfo.iexn -> Exninfo.iexn)
+ -> Evd.evar_map
-> GlobRef.t
val declare_assumption
@@ -97,17 +113,6 @@ val declare_mutually_recursive
-> Recthm.t list
-> Names.GlobRef.t list
-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
- -> ClosedDef.t
-
val prepare_obligation
: ?opaque:bool
-> ?inline:bool
diff --git a/vernac/declareObl.ml b/vernac/declareObl.ml
index 4c62582c23..bba3687256 100644
--- a/vernac/declareObl.ml
+++ b/vernac/declareObl.ml
@@ -371,9 +371,12 @@ let declare_definition prg =
let fix_exn = Hook.get get_fix_exn () in
let obls = List.map (fun (id, (_, c)) -> (id, c)) varsubst in
(* XXX: This is doing normalization twice *)
- let ce = DeclareDef.prepare_definition ~fix_exn ~opaque ~poly ~udecl ~types ~body sigma in
let () = progmap_remove prg in
- DeclareDef.declare_definition ~name ~scope ~kind ~impargs ?hook ~obls ce
+ let kn =
+ DeclareDef.declare_definition ~name ~scope ~kind ~impargs ?hook ~obls
+ ~fix_exn ~opaque ~poly ~udecl ~types ~body sigma
+ in
+ kn
let rec lam_index n t acc =
match Constr.kind t with
diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml
index ee4fc4334e..feedf4d71d 100644
--- a/vernac/lemmas.ml
+++ b/vernac/lemmas.ml
@@ -238,8 +238,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 ~uctx pe in
- DeclareDef.declare_definition ~name ~scope ~kind ?hook ~impargs pe
+ DeclareDef.declare_entry ~name ~scope ~kind ?hook ~impargs ~uctx pe
let declare_mutdef ~info ~uctx const =
let pe = match info.Info.compute_guard with
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 12:51:40 +0000