aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--doc/plugin_tutorial/tuto1/src/simple_declare.ml4
-rw-r--r--plugins/ltac/rewrite.ml3
-rw-r--r--vernac/classes.ml11
-rw-r--r--vernac/comDefinition.ml4
-rw-r--r--vernac/comDefinition.mli2
-rw-r--r--vernac/comFixpoint.ml5
-rw-r--r--vernac/comProgramFixpoint.ml4
-rw-r--r--vernac/declare.ml139
-rw-r--r--vernac/declare.mli78
-rw-r--r--vernac/obligations.ml41
-rw-r--r--vernac/obligations.mli4
-rw-r--r--vernac/vernacentries.ml1
12 files changed, 156 insertions, 140 deletions
diff --git a/doc/plugin_tutorial/tuto1/src/simple_declare.ml b/doc/plugin_tutorial/tuto1/src/simple_declare.ml
index e9e866c5fb..5431a21b53 100644
--- a/doc/plugin_tutorial/tuto1/src/simple_declare.ml
+++ b/doc/plugin_tutorial/tuto1/src/simple_declare.ml
@@ -2,5 +2,5 @@ let declare_definition ~poly name sigma body =
let udecl = UState.default_univ_decl in
let scope = Declare.Global Declare.ImportDefaultBehavior in
let kind = Decls.(IsDefinition Definition) in
- Declare.declare_definition ~name ~scope ~kind ~impargs:[] ~udecl
- ~opaque:false ~poly ~types:None ~body sigma
+ let info = Declare.CInfo.make ~scope ~kind ~impargs:[] ~udecl ~opaque:false ~poly () in
+ Declare.declare_definition ~name ~info ~types:None ~body sigma
diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml
index 914dc96648..67d09acfda 100644
--- a/plugins/ltac/rewrite.ml
+++ b/plugins/ltac/rewrite.ml
@@ -1902,8 +1902,9 @@ let declare_projection name instance_id r =
let types = Some (it_mkProd_or_LetIn typ ctx) in
let kind, opaque, scope = Decls.(IsDefinition Definition), false, Declare.Global Declare.ImportDefaultBehavior in
let impargs, udecl = [], UState.default_univ_decl in
+ let info = Declare.CInfo.make ~scope ~kind ~opaque ~impargs ~udecl ~poly () in
let _r : GlobRef.t =
- Declare.declare_definition ~name ~scope ~kind ~opaque ~impargs ~udecl ~poly ~types ~body sigma
+ Declare.declare_definition ~name ~info ~types ~body sigma
in ()
let build_morphism_signature env sigma m =
diff --git a/vernac/classes.ml b/vernac/classes.ml
index f7d8a4b42f..c4c6a0fa33 100644
--- a/vernac/classes.ml
+++ b/vernac/classes.ml
@@ -311,12 +311,12 @@ let instance_hook info global ?hook cst =
declare_instance env sigma (Some info) (not global) cst;
(match hook with Some h -> h cst | None -> ())
-let declare_instance_constant info global impargs ?hook name udecl poly sigma term termtype =
+let declare_instance_constant iinfo global impargs ?hook name udecl poly sigma term termtype =
let kind = Decls.(IsDefinition Instance) in
let scope = Declare.Global Declare.ImportDefaultBehavior in
- let kn = Declare.declare_definition ~name ~kind ~scope ~impargs
- ~opaque:false ~poly sigma ~udecl ~types:(Some termtype) ~body:term in
- instance_hook info global ?hook kn
+ let info = Declare.CInfo.make ~kind ~scope ~impargs ~opaque:false ~poly ~udecl () in
+ let kn = Declare.declare_definition ~name ~info ~types:(Some termtype) ~body:term sigma in
+ instance_hook iinfo global ?hook kn
let do_declare_instance sigma ~global ~poly k u ctx ctx' pri udecl impargs subst name =
let subst = List.fold_left2
@@ -344,7 +344,8 @@ let declare_instance_program env sigma ~global ~poly name pri impargs udecl term
let obls, _, term, typ = RetrieveObl.retrieve_obligations env name sigma 0 term termtype in
let hook = Declare.Hook.make hook in
let uctx = Evd.evar_universe_context sigma in
- let scope, kind = Declare.Global Declare.ImportDefaultBehavior, Decls.Instance in
+ let scope, kind = Declare.Global Declare.ImportDefaultBehavior,
+ Decls.IsDefinition Decls.Instance in
let _ : Declare.progress =
Obligations.add_definition ~name ~term ~udecl ~scope ~poly ~kind ~hook ~impargs ~uctx typ obls
in ()
diff --git a/vernac/comDefinition.ml b/vernac/comDefinition.ml
index a791e67bb1..c89de88e95 100644
--- a/vernac/comDefinition.ml
+++ b/vernac/comDefinition.ml
@@ -116,9 +116,9 @@ let do_definition ?hook ~name ~scope ~poly ~kind udecl bl red_option c ctypopt =
interp_definition ~program_mode udecl bl ~poly red_option c ctypopt
in
let kind = Decls.IsDefinition kind in
+ let info = Declare.CInfo.make ~scope ~kind ?hook ~opaque:false ~impargs ~udecl ~poly () in
let _ : Names.GlobRef.t =
- Declare.declare_definition ~name ~scope ~kind ?hook ~impargs
- ~opaque:false ~poly evd ~udecl ~types ~body
+ Declare.declare_definition ~name ~info ~types ~body evd
in ()
let do_definition_program ?hook ~name ~scope ~poly ~kind udecl bl red_option c ctypopt =
diff --git a/vernac/comDefinition.mli b/vernac/comDefinition.mli
index 2e8fe16252..2b846f17e0 100644
--- a/vernac/comDefinition.mli
+++ b/vernac/comDefinition.mli
@@ -32,7 +32,7 @@ val do_definition_program
-> name:Id.t
-> scope:Declare.locality
-> poly:bool
- -> kind:Decls.definition_object_kind
+ -> kind:Decls.logical_kind
-> universe_decl_expr option
-> local_binder_expr list
-> red_expr option
diff --git a/vernac/comFixpoint.ml b/vernac/comFixpoint.ml
index 5bf3350777..925a2d8389 100644
--- a/vernac/comFixpoint.ml
+++ b/vernac/comFixpoint.ml
@@ -283,9 +283,10 @@ let declare_fixpoint_generic ?indexes ~scope ~poly ((fixnames,fixrs,fixdefs,fixt
let fixdefs = List.map Option.get fixdefs in
let rec_declaration = prepare_recursive_declaration fixnames fixrs fixtypes fixdefs in
let fix_kind = Decls.IsDefinition fix_kind in
+ let info = Declare.CInfo.make ~scope ~opaque:false ~kind:fix_kind ~poly ~udecl () in
let _ : GlobRef.t list =
- Declare.declare_mutually_recursive ~scope ~opaque:false ~kind:fix_kind ~poly ~uctx
- ~possible_indexes:indexes ~udecl ~ntns ~rec_declaration
+ Declare.declare_mutually_recursive ~info ~uctx
+ ~possible_indexes:indexes ~ntns ~rec_declaration
fixitems
in
()
diff --git a/vernac/comProgramFixpoint.ml b/vernac/comProgramFixpoint.ml
index 4aa46e0a86..e51a786cb0 100644
--- a/vernac/comProgramFixpoint.ml
+++ b/vernac/comProgramFixpoint.ml
@@ -314,8 +314,8 @@ let do_program_recursive ~scope ~poly fixkind fixl =
end in
let uctx = Evd.evar_universe_context evd in
let kind = match fixkind with
- | Declare.Obls.IsFixpoint _ -> Decls.Fixpoint
- | Declare.Obls.IsCoFixpoint -> Decls.CoFixpoint
+ | Declare.Obls.IsFixpoint _ -> Decls.(IsDefinition Fixpoint)
+ | Declare.Obls.IsCoFixpoint -> Decls.(IsDefinition CoFixpoint)
in
let ntns = List.map_append (fun { Vernacexpr.notations } -> notations ) fixl in
Obligations.add_mutual_definitions defs ~poly ~scope ~kind ~udecl ~uctx ntns fixkind
diff --git a/vernac/declare.ml b/vernac/declare.ml
index ebea919f64..5c5e03fd89 100644
--- a/vernac/declare.ml
+++ b/vernac/declare.ml
@@ -1037,6 +1037,26 @@ let declare_universe_context = DeclareUctx.declare_universe_context
type locality = Locality.locality = | Discharge | Global of import_status
+module CInfo = struct
+
+ type t =
+ { poly : bool
+ ; opaque : bool
+ ; inline : bool
+ ; kind : Decls.logical_kind
+ ; udecl : UState.universe_decl
+ ; scope : locality
+ ; impargs : Impargs.manual_implicits
+ ; hook : Hook.t option
+ }
+
+ let make ?(poly=false) ?(opaque=false) ?(inline=false) ?(kind=Decls.(IsDefinition Definition))
+ ?(udecl=UState.default_univ_decl) ?(scope=Global ImportNeedQualified) ?(impargs=[])
+ ?hook () =
+ { poly; opaque; inline; kind; udecl; scope; impargs; hook }
+
+end
+
(* Locality stuff *)
let declare_entry_core ~name ~scope ~kind ?hook ~obls ~impargs ~uctx entry =
let should_suggest =
@@ -1077,7 +1097,8 @@ let mutual_make_bodies ~fixitems ~rec_declaration ~possible_indexes =
let vars = Vars.universes_of_constr (List.hd fixdecls) in
vars, fixdecls, None
-let declare_mutually_recursive_core ~opaque ~scope ~kind ~poly ~uctx ~udecl ~ntns ~rec_declaration ~possible_indexes ?(restrict_ucontext=true) fixitems =
+let declare_mutually_recursive_core ~info ~ntns ~uctx ~rec_declaration ~possible_indexes ?(restrict_ucontext=true) fixitems =
+ let { CInfo.poly; udecl; opaque; scope; kind; _ } = info in
let vars, fixdecls, indexes =
mutual_make_bodies ~fixitems ~rec_declaration ~possible_indexes in
let uctx, univs =
@@ -1127,20 +1148,21 @@ let declare_assumption ~name ~scope ~hook ~impargs ~uctx pe =
(* Preparing proof entries *)
-let prepare_definition ?opaque ?inline ~poly ~udecl ~types ~body sigma =
+let prepare_definition ~info ~types ~body sigma =
+ let { CInfo.poly; udecl; opaque; inline; _ } = info in
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
- let entry = definition_entry ?opaque ?inline ?types ~univs body in
+ let entry = definition_entry ~opaque ~inline ?types ~univs body in
let uctx = Evd.evar_universe_context sigma in
entry, uctx
-let declare_definition_core ~name ~scope ~kind ~opaque ~impargs ~udecl ?hook
- ~obls ~poly ?inline ~types ~body sigma =
- let entry, uctx = prepare_definition ~opaque ~poly ~udecl ~types ~body ?inline sigma in
+let declare_definition_core ~name ~info ~obls ~types ~body sigma =
+ let entry, uctx = prepare_definition ~info ~types ~body sigma in
+ let { CInfo.scope; kind; impargs; hook; _ } = info in
declare_entry_core ~name ~scope ~kind ~impargs ~obls ?hook ~uctx entry
let declare_definition = declare_definition_core ~obls:[]
@@ -1196,37 +1218,32 @@ type obligations = {obls : Obligation.t array; remaining : int}
type fixpoint_kind = IsFixpoint of lident option list | IsCoFixpoint
module ProgramDecl = struct
+
type t =
{ prg_name : Id.t
+ ; prg_info : CInfo.t
; prg_body : constr
; prg_type : constr
- ; prg_ctx : UState.t
- ; prg_univdecl : UState.universe_decl
+ ; prg_uctx : UState.t
; prg_obligations : obligations
; prg_deps : Id.t list
; prg_fixkind : fixpoint_kind option
- ; prg_implicits : Impargs.manual_implicits
; prg_notations : Vernacexpr.decl_notation list
- ; prg_poly : bool
- ; prg_scope : locality
- ; prg_kind : Decls.definition_object_kind
; prg_reduce : constr -> constr
- ; prg_hook : Hook.t option
- ; prg_opaque : bool }
+ }
open Obligation
- let make ?(opaque = false) ?hook n ~udecl ~uctx ~impargs ~poly ~scope ~kind b
- t deps fixkind notations obls reduce =
- let obls', b =
- match b with
+ let make prg_name ~info ~ntns ~reduce ~deps ~uctx ~types ~body fixkind obls =
+ let obls', body =
+ match body with
| None ->
assert (Int.equal (Array.length obls) 0);
- let n = Nameops.add_suffix n "_obligation" in
+ let n = Nameops.add_suffix prg_name "_obligation" in
( [| { obl_name = n
; obl_body = None
; obl_location = Loc.tag Evar_kinds.InternalHole
- ; obl_type = t
+ ; obl_type = types
; obl_status = (false, Evar_kinds.Expand)
; obl_deps = Int.Set.empty
; obl_tac = None } |]
@@ -1244,25 +1261,23 @@ module ProgramDecl = struct
obls
, b )
in
- let ctx = UState.make_flexible_nonalgebraic uctx in
- { prg_name = n
- ; prg_body = b
- ; prg_type = reduce t
- ; prg_ctx = ctx
- ; prg_univdecl = udecl
+ let prg_uctx = UState.make_flexible_nonalgebraic uctx in
+ { prg_name
+ ; prg_info = info
+ ; prg_body = body
+ ; prg_type = reduce types
+ ; prg_uctx
; prg_obligations = {obls = obls'; remaining = Array.length obls'}
; prg_deps = deps
; prg_fixkind = fixkind
- ; prg_notations = notations
- ; prg_implicits = impargs
- ; prg_poly = poly
- ; prg_scope = scope
- ; prg_kind = kind
- ; prg_reduce = reduce
- ; prg_hook = hook
- ; prg_opaque = opaque }
-
- let set_uctx ~uctx prg = {prg with prg_ctx = uctx}
+ ; prg_notations = ntns
+ ; prg_reduce = reduce }
+
+ module Internal = struct
+ let get_uctx prg = prg.prg_uctx
+ let get_poly prg = prg.prg_info.CInfo.poly
+ let set_uctx ~uctx prg = {prg with prg_uctx = uctx}
+ end
end
open Obligation
@@ -1349,14 +1364,15 @@ let get_hide_obligations =
~value:false
let declare_obligation prg obl ~uctx ~types ~body =
- let univs = UState.univ_entry ~poly:prg.prg_poly uctx in
+ let poly = prg.prg_info.CInfo.poly in
+ let univs = UState.univ_entry ~poly uctx in
let body = prg.prg_reduce body in
let types = Option.map prg.prg_reduce types in
match obl.obl_status with
| _, Evar_kinds.Expand -> (false, {obl with obl_body = Some (TermObl body)})
| force, Evar_kinds.Define opaque ->
let opaque = (not force) && opaque in
- let poly = prg.prg_poly in
+ let poly = prg.prg_info.CInfo.poly in
let ctx, body, ty, args =
if not poly then shrink_body body types
else ([], body, types, [||])
@@ -1562,25 +1578,13 @@ let subst_prog subst prg =
let declare_definition prg =
let varsubst = obligation_substitution true prg in
- let sigma = Evd.from_ctx prg.prg_ctx in
+ let sigma = Evd.from_ctx prg.prg_uctx in
let body, types = subst_prog varsubst prg in
let body, types = EConstr.(of_constr body, Some (of_constr types)) in
- (* All these should be grouped into a struct a some point *)
- let opaque, poly, udecl, hook =
- (prg.prg_opaque, prg.prg_poly, prg.prg_univdecl, prg.prg_hook)
- in
- let name, scope, kind, impargs =
- ( prg.prg_name
- , prg.prg_scope
- , Decls.(IsDefinition prg.prg_kind)
- , prg.prg_implicits )
- in
+ let name, info = prg.prg_name, prg.prg_info in
let obls = List.map (fun (id, (_, c)) -> (id, c)) varsubst in
(* XXX: This is doing normalization twice *)
- let kn =
- declare_definition_core ~name ~scope ~kind ~impargs ?hook ~obls
- ~opaque ~poly ~udecl ~types ~body sigma
- in
+ let kn = declare_definition_core ~name ~info ~obls ~types ~body sigma in
let pm = progmap_remove !State.prg_ref prg in
State.prg_ref := pm;
kn
@@ -1611,7 +1615,7 @@ let declare_mutual_definition l =
let oblsubst = obligation_substitution true x in
let subs, typ = subst_prog oblsubst x in
let env = Global.env () in
- let sigma = Evd.from_ctx x.prg_ctx in
+ let sigma = Evd.from_ctx x.prg_uctx in
let r = Retyping.relevance_of_type env sigma (EConstr.of_constr typ) in
let term =
snd (Reductionops.splay_lam_n env sigma len (EConstr.of_constr subs))
@@ -1621,7 +1625,7 @@ let declare_mutual_definition l =
in
let term = EConstr.to_constr sigma term in
let typ = EConstr.to_constr sigma typ in
- let def = (x.prg_reduce term, r, x.prg_reduce typ, x.prg_implicits) in
+ let def = (x.prg_reduce term, r, x.prg_reduce typ, x.prg_info.CInfo.impargs) in
let oblsubst = List.map (fun (id, (_, c)) -> (id, c)) oblsubst in
(def, oblsubst)
in
@@ -1654,24 +1658,22 @@ let declare_mutual_definition l =
| IsCoFixpoint -> None
in
(* In the future we will pack all this in a proper record *)
- let poly, scope, ntns, opaque =
- (first.prg_poly, first.prg_scope, first.prg_notations, first.prg_opaque)
- in
- let kind =
+ (* XXX: info refactoring *)
+ let _kind =
if fixkind != IsCoFixpoint then Decls.(IsDefinition Fixpoint)
else Decls.(IsDefinition CoFixpoint)
in
+ let scope = first.prg_info.CInfo.scope in
(* Declare the recursive definitions *)
- let udecl = UState.default_univ_decl in
let kns =
- declare_mutually_recursive_core ~scope ~opaque ~kind ~udecl ~ntns
- ~uctx:first.prg_ctx ~rec_declaration ~possible_indexes ~poly
+ declare_mutually_recursive_core ~info:first.prg_info ~ntns:first.prg_notations
+ ~uctx:first.prg_uctx ~rec_declaration ~possible_indexes
~restrict_ucontext:false fixitems
in
(* Only for the first constant *)
let dref = List.hd kns in
Hook.(
- call ?hook:first.prg_hook {S.uctx = first.prg_ctx; obls; scope; dref});
+ call ?hook:first.prg_info.CInfo.hook {S.uctx = first.prg_uctx; obls; scope; dref});
let pm = List.fold_left progmap_remove !State.prg_ref l in
State.prg_ref := pm;
dref
@@ -1711,7 +1713,7 @@ let dependencies obls n =
let update_program_decl_on_defined prg obls num obl ~uctx rem ~auto =
let obls = Array.copy obls in
let () = obls.(num) <- obl in
- let prg = {prg with prg_ctx = uctx} in
+ let prg = {prg with prg_uctx = uctx} in
let _progress = update_obls prg obls (pred rem) in
let () =
if pred rem > 0 then
@@ -1746,14 +1748,15 @@ let obligation_terminator entries uctx {name; num; auto} =
| (_, status), false -> status
in
let obl = {obl with obl_status = (false, status)} in
- let uctx = if prg.prg_poly then uctx else UState.union prg.prg_ctx uctx in
+ let poly = prg.prg_info.CInfo.poly in
+ let uctx = if poly then uctx else UState.union prg.prg_uctx uctx in
let defined, obl = declare_obligation prg obl ~body ~types:ty ~uctx in
let prg_ctx =
- if prg.prg_poly then
+ if poly then
(* Polymorphic *)
(* We merge the new universes and constraints of the
polymorphic obligation with the existing ones *)
- UState.union prg.prg_ctx uctx
+ UState.union prg.prg_uctx uctx
else if
(* The first obligation, if defined,
declares the univs of the constant,
@@ -1790,7 +1793,7 @@ let obligation_admitted_terminator {name; num; auto} ctx' dref =
| _ -> ()
in
let inst, ctx' =
- if not prg.prg_poly (* Not polymorphic *) then
+ if not prg.prg_info.CInfo.poly (* Not polymorphic *) then
(* The universe context was declared globally, we continue
from the new global environment. *)
let ctx = UState.from_env (Global.env ()) in
diff --git a/vernac/declare.mli b/vernac/declare.mli
index 55c6175371..30db26e693 100644
--- a/vernac/declare.mli
+++ b/vernac/declare.mli
@@ -354,6 +354,28 @@ val declare_universe_context : poly:bool -> Univ.ContextSet.t -> unit
type locality = Locality.locality = Discharge | Global of import_status
+(** Information for a constant *)
+module CInfo : sig
+
+ type t
+
+ val make :
+ ?poly:bool
+ -> ?opaque : bool
+ -> ?inline : bool
+ -> ?kind : Decls.logical_kind
+ (** Theorem, etc... *)
+ -> ?udecl : UState.universe_decl
+ -> ?scope : locality
+ (** locality *)
+ -> ?impargs : Impargs.manual_implicits
+ -> ?hook : Hook.t
+ (** Callback to be executed after saving the constant *)
+ -> unit
+ -> t
+
+end
+
(** XXX: This is an internal, low-level API and could become scheduled
for removal from the public API, use higher-level declare APIs
instead *)
@@ -375,14 +397,7 @@ val declare_entry
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
- -> poly:bool
- -> ?inline:bool
+ -> info:CInfo.t
-> types:EConstr.t option
-> body:EConstr.t
-> Evd.evar_map
@@ -398,13 +413,9 @@ val declare_assumption
-> GlobRef.t
val declare_mutually_recursive
- : opaque:bool
- -> scope:locality
- -> kind:Decls.logical_kind
- -> poly:bool
- -> uctx:UState.t
- -> udecl:UState.universe_decl
+ : info:CInfo.t
-> ntns:Vernacexpr.decl_notation list
+ -> uctx:UState.t
-> rec_declaration:Constr.rec_declaration
-> possible_indexes:lemma_possible_guards option
-> Recthm.t list
@@ -453,42 +464,37 @@ type fixpoint_kind = IsFixpoint of lident option list | IsCoFixpoint
module ProgramDecl : sig
type t = private
{ prg_name : Id.t
+ ; prg_info : CInfo.t
; prg_body : constr
; prg_type : constr
- ; prg_ctx : UState.t
- ; prg_univdecl : UState.universe_decl
+ ; prg_uctx : UState.t
; prg_obligations : obligations
; prg_deps : Id.t list
; prg_fixkind : fixpoint_kind option
- ; prg_implicits : Impargs.manual_implicits
; prg_notations : Vernacexpr.decl_notation list
- ; prg_poly : bool
- ; prg_scope : locality
- ; prg_kind : Decls.definition_object_kind
; prg_reduce : constr -> constr
- ; prg_hook : Hook.t option
- ; prg_opaque : bool }
+ }
val make :
- ?opaque:bool
- -> ?hook:Hook.t
- -> Names.Id.t
- -> udecl:UState.universe_decl
+ Names.Id.t
+ -> info:CInfo.t
+ -> ntns:Vernacexpr.decl_notation list
+ -> reduce:(Constr.constr -> Constr.constr)
+ -> deps:Names.Id.t list
-> uctx:UState.t
- -> impargs:Impargs.manual_implicits
- -> poly:bool
- -> scope:locality
- -> kind:Decls.definition_object_kind
- -> Constr.constr option
- -> Constr.types
- -> Names.Id.t list
+ -> types:Constr.types
+ -> body:Constr.constr option
-> fixpoint_kind option
- -> Vernacexpr.decl_notation list
-> RetrieveObl.obligation_info
- -> (Constr.constr -> Constr.constr)
-> t
- val set_uctx : uctx:UState.t -> t -> t
+ (* This is internal, only here as obligations get merged into the
+ regular declaration path *)
+ module Internal : sig
+ val get_poly : t -> bool
+ val get_uctx : t -> UState.t
+ val set_uctx : uctx:UState.t -> t -> t
+ end
end
(** [declare_obligation prg obl ~uctx ~types ~body] Save an obligation
diff --git a/vernac/obligations.ml b/vernac/obligations.ml
index 62fdbf50ad..83ea6c21f0 100644
--- a/vernac/obligations.ml
+++ b/vernac/obligations.ml
@@ -95,7 +95,7 @@ let warn_solve_errored =
; fnl ()
; str "This will become an error in the future" ])
-let solve_by_tac ?loc name evi t poly uctx =
+let solve_by_tac ?loc name evi t ~poly ~uctx =
(* the status is dropped. *)
try
let env = Global.env () in
@@ -137,7 +137,7 @@ let rec solve_obligation prg num tac =
let obl = subst_deps_obl obls obl in
let scope = Declare.(Global Declare.ImportNeedQualified) in
let kind = kind_of_obligation (snd obl.obl_status) in
- let evd = Evd.from_ctx prg.prg_ctx in
+ let evd = Evd.from_ctx prg.prg_uctx in
let evd = Evd.update_sigma_env evd (Global.env ()) in
let auto n oblset tac = auto_solve_obligations n ~oblset tac in
let proof_ending =
@@ -145,7 +145,7 @@ let rec solve_obligation prg num tac =
{Declare.name = prg.prg_name; num; auto}
in
let info = Declare.Info.make ~proof_ending ~scope ~kind () in
- let poly = prg.prg_poly in
+ let poly = Internal.get_poly prg in
let lemma = Declare.start_proof ~name:obl.obl_name ~poly ~impargs:[] ~udecl:UState.default_univ_decl ~info evd (EConstr.of_constr obl.obl_type) in
let lemma = fst @@ Declare.by !default_tactic lemma in
let lemma = Option.cata (fun tac -> Declare.Proof.set_endline_tactic tac lemma) lemma tac in
@@ -177,21 +177,20 @@ and solve_obligation_by_tac prg obls i tac =
| Some t -> t
| None -> !default_tactic
in
- let evd = Evd.from_ctx prg.prg_ctx in
- let evd = Evd.update_sigma_env evd (Global.env ()) in
- match solve_by_tac ?loc:(fst obl.obl_location) obl.obl_name (evar_of_obligation obl) tac
- prg.prg_poly (Evd.evar_universe_context evd) with
+ let uctx = Internal.get_uctx prg in
+ let uctx = UState.update_sigma_env uctx (Global.env ()) in
+ let poly = Internal.get_poly prg in
+ match solve_by_tac ?loc:(fst obl.obl_location) obl.obl_name (evar_of_obligation obl) tac ~poly ~uctx with
| None -> None
| Some (t, ty, uctx) ->
- let prg = ProgramDecl.set_uctx ~uctx prg in
- (* Why is uctx not used above? *)
+ let prg = ProgramDecl.Internal.set_uctx ~uctx prg in
let def, obl' = declare_obligation prg obl ~body:t ~types:ty ~uctx in
obls.(i) <- obl';
- if def && not prg.prg_poly then (
+ if def && not poly then (
(* Declare the term constraints with the first obligation only *)
let uctx_global = UState.from_env (Global.env ()) in
let uctx = UState.merge_subst uctx_global (UState.subst uctx) in
- Some (ProgramDecl.set_uctx ~uctx prg))
+ Some (ProgramDecl.Internal.set_uctx ~uctx prg))
else Some prg
else None
@@ -313,9 +312,12 @@ let msg_generating_obl name obls =
let add_definition ~name ?term t ~uctx ?(udecl = UState.default_univ_decl)
?(impargs = []) ~poly
?(scope = Declare.Global Declare.ImportDefaultBehavior)
- ?(kind = Decls.Definition) ?tactic ?(reduce = reduce) ?hook
+ ?(kind = Decls.(IsDefinition Definition)) ?tactic ?(reduce = reduce) ?hook
?(opaque = false) obls =
- let prg = ProgramDecl.make ~opaque name ~udecl term t ~uctx [] None [] obls ~impargs ~poly ~scope ~kind reduce ?hook in
+ let prg =
+ let info = Declare.CInfo.make ~poly ~opaque ~udecl ~impargs ~scope ~kind ?hook () in
+ ProgramDecl.make name ~info ~body:term ~types:t ~uctx ~reduce ~ntns:[] ~deps:[] None obls
+ in
let {obls;_} = prg.prg_obligations in
if Int.equal (Array.length obls) 0 then (
Flags.if_verbose (msg_generating_obl name) obls;
@@ -333,16 +335,16 @@ let add_definition ~name ?term t ~uctx ?(udecl = UState.default_univ_decl)
let add_mutual_definitions l ~uctx ?(udecl = UState.default_univ_decl)
?tactic ~poly ?(scope = Declare.Global Declare.ImportDefaultBehavior)
- ?(kind = Decls.Definition) ?(reduce = reduce) ?hook ?(opaque = false)
+ ?(kind = Decls.(IsDefinition Definition)) ?(reduce = reduce) ?hook ?(opaque = false)
notations fixkind =
let deps = List.map (fun ({Declare.Recthm.name; _}, _, _) -> name) l in
let pm =
List.fold_left
(fun () ({Declare.Recthm.name; typ; impargs; _}, b, obls) ->
+ let info = Declare.CInfo.make ~impargs ~poly ~scope ~kind ~opaque ~udecl ?hook () in
let prg =
- ProgramDecl.make ~opaque name ~udecl (Some b) typ ~uctx deps
- (Some fixkind) notations obls ~impargs ~poly ~scope ~kind reduce
- ?hook
+ ProgramDecl.make name ~info ~body:(Some b) ~types:typ ~uctx ~deps
+ (Some fixkind) ~ntns:notations obls ~reduce
in
State.add name prg)
() l
@@ -371,9 +373,10 @@ let admit_prog prg =
match x.obl_body with
| None ->
let x = subst_deps_obl obls x in
- let ctx = UState.univ_entry ~poly:false prg.prg_ctx in
+ let uctx = Internal.get_uctx prg in
+ let univs = UState.univ_entry ~poly:false uctx in
let kn = Declare.declare_constant ~name:x.obl_name ~local:Declare.ImportNeedQualified
- (Declare.ParameterEntry (None, (x.obl_type, ctx), None)) ~kind:Decls.(IsAssumption Conjectural)
+ (Declare.ParameterEntry (None, (x.obl_type, univs), None)) ~kind:Decls.(IsAssumption Conjectural)
in
Declare.assumption_message x.obl_name;
obls.(i) <- Obligation.set_body ~body:(DefinedObl (kn, Univ.Instance.empty)) x
diff --git a/vernac/obligations.mli b/vernac/obligations.mli
index f0a8e9bea1..76e2f5cb2c 100644
--- a/vernac/obligations.mli
+++ b/vernac/obligations.mli
@@ -78,7 +78,7 @@ val add_definition :
-> ?impargs:Impargs.manual_implicits
-> poly:bool
-> ?scope:Declare.locality
- -> ?kind:Decls.definition_object_kind
+ -> ?kind:Decls.logical_kind
-> ?tactic:unit Proofview.tactic
-> ?reduce:(constr -> constr)
-> ?hook:Declare.Hook.t
@@ -97,7 +97,7 @@ val add_mutual_definitions :
-> ?tactic:unit Proofview.tactic
-> poly:bool
-> ?scope:Declare.locality
- -> ?kind:Decls.definition_object_kind
+ -> ?kind:Decls.logical_kind
-> ?reduce:(constr -> constr)
-> ?hook:Declare.Hook.t
-> ?opaque:bool
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 1ada477d07..f7da2000e3 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -577,6 +577,7 @@ let vernac_definition ~atts (discharge, kind) (lid, pl) bl red_option c typ_opt
let sigma = Evd.from_env env in
Some (snd (Hook.get f_interp_redexp env sigma r)) in
if program_mode then
+ let kind = Decls.IsDefinition kind in
ComDefinition.do_definition_program ~name:name.v
~poly:atts.polymorphic ~scope ~kind pl bl red_option c typ_opt ?hook
else
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 12:48:58 +0000