aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--doc/plugin_tutorial/tuto1/src/simple_declare.ml5
-rw-r--r--plugins/derive/derive.ml5
-rw-r--r--plugins/funind/functional_principles_proofs.ml6
-rw-r--r--plugins/funind/gen_principle.ml12
-rw-r--r--plugins/funind/recdef.ml25
-rw-r--r--plugins/ltac/rewrite.ml10
-rw-r--r--stm/stm.ml19
-rw-r--r--vernac/classes.ml10
-rw-r--r--vernac/comDefinition.ml5
-rw-r--r--vernac/comFixpoint.ml19
-rw-r--r--vernac/comProgramFixpoint.ml3
-rw-r--r--vernac/declare.ml341
-rw-r--r--vernac/declare.mli137
-rw-r--r--vernac/obligations.ml22
-rw-r--r--vernac/obligations.mli2
-rw-r--r--vernac/recLemmas.ml7
-rw-r--r--vernac/recLemmas.mli6
-rw-r--r--vernac/vernacentries.ml15
-rw-r--r--vernac/vernacinterp.ml14
-rw-r--r--vernac/vernacinterp.mli2
-rw-r--r--vernac/vernacstate.ml3
-rw-r--r--vernac/vernacstate.mli2
22 files changed, 336 insertions, 334 deletions
diff --git a/doc/plugin_tutorial/tuto1/src/simple_declare.ml b/doc/plugin_tutorial/tuto1/src/simple_declare.ml
index 73292e0120..4d0105ea9d 100644
--- a/doc/plugin_tutorial/tuto1/src/simple_declare.ml
+++ b/doc/plugin_tutorial/tuto1/src/simple_declare.ml
@@ -2,5 +2,6 @@ let declare_definition ~poly name sigma body =
let udecl = UState.default_univ_decl in
let scope = Locality.Global Locality.ImportDefaultBehavior in
let kind = Decls.(IsDefinition Definition) in
- let info = Declare.CInfo.make ~scope ~kind ~impargs:[] ~udecl ~opaque:false ~poly () in
- Declare.declare_definition ~name ~info ~types:None ~body sigma
+ let cinfo = Declare.CInfo.make ~name ~typ:None () in
+ let info = Declare.Info.make ~scope ~kind ~udecl ~poly () in
+ Declare.declare_definition ~info ~cinfo ~opaque:false ~body sigma
diff --git a/plugins/derive/derive.ml b/plugins/derive/derive.ml
index d85d3bd744..27df963e98 100644
--- a/plugins/derive/derive.ml
+++ b/plugins/derive/derive.ml
@@ -40,7 +40,8 @@ let start_deriving f suchthat name : Declare.Proof.t =
TNil sigma))))))
in
- let info = Declare.Info.make ~proof_ending:(Declare.Proof_ending.(End_derive {f; name})) ~kind () in
- let lemma = Declare.Proof.start_dependent ~name ~poly ~info goals in
+ let info = Declare.Info.make ~poly ~kind () in
+ let proof_ending = Declare.Proof_ending.(End_derive {f; name}) in
+ let lemma = Declare.Proof.start_dependent ~name ~info ~proof_ending goals in
Declare.Proof.map lemma ~f:(fun p ->
Util.pi1 @@ Proof.run_tactic env Proofview.(tclFOCUS 1 2 shelve) p)
diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml
index 79f311e282..afe89aef6e 100644
--- a/plugins/funind/functional_principles_proofs.ml
+++ b/plugins/funind/functional_principles_proofs.ml
@@ -854,10 +854,10 @@ let generate_equation_lemma evd fnames f fun_num nb_params nb_args rec_args_num
(*i The next call to mk_equation_id is valid since we are
constructing the lemma Ensures by: obvious i*)
let info = Declare.Info.make () in
- let lemma =
- Declare.Proof.start ~name:(mk_equation_id f_id) ~poly:false ~info
- ~impargs:[] evd lemma_type
+ let cinfo =
+ Declare.CInfo.make ~name:(mk_equation_id f_id) ~typ:lemma_type ()
in
+ let lemma = Declare.Proof.start ~cinfo ~info evd in
let lemma, _ =
Declare.Proof.by (Proofview.V82.tactic prove_replacement) lemma
in
diff --git a/plugins/funind/gen_principle.ml b/plugins/funind/gen_principle.ml
index 50ce783579..0cd5df12f7 100644
--- a/plugins/funind/gen_principle.ml
+++ b/plugins/funind/gen_principle.ml
@@ -1519,10 +1519,8 @@ let derive_correctness (funs : Constr.pconstant list) (graphs : inductive list)
let lem_id = mk_correct_id f_id in
let typ, _ = lemmas_types_infos.(i) in
let info = Declare.Info.make () in
- let lemma =
- Declare.Proof.start ~name:lem_id ~poly:false ~info ~impargs:[] !evd
- typ
- in
+ let cinfo = Declare.CInfo.make ~name:lem_id ~typ () in
+ let lemma = Declare.Proof.start ~cinfo ~info !evd in
let lemma =
fst @@ Declare.Proof.by (Proofview.V82.tactic (proving_tac i)) lemma
in
@@ -1585,10 +1583,10 @@ let derive_correctness (funs : Constr.pconstant list) (graphs : inductive list)
i*)
let lem_id = mk_complete_id f_id in
let info = Declare.Info.make () in
- let lemma =
- Declare.Proof.start ~name:lem_id ~poly:false sigma ~info ~impargs:[]
- (fst lemmas_types_infos.(i))
+ let cinfo =
+ Declare.CInfo.make ~name:lem_id ~typ:(fst lemmas_types_infos.(i)) ()
in
+ let lemma = Declare.Proof.start ~cinfo sigma ~info in
let lemma =
fst
(Declare.Proof.by
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index 5a188ca82b..92eb85ffd8 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -1492,10 +1492,8 @@ let open_new_goal ~lemma build_proof sigma using_lemmas ref_ goal_name
Declare.Proof.save ~proof:lemma ~opaque:opacity ~idopt:None
in
let info = Declare.Info.make ~hook:(Declare.Hook.make hook) () in
- let lemma =
- Declare.Proof.start ~name:na ~poly:false (* FIXME *) ~info ~impargs:[] sigma
- gls_type
- in
+ let cinfo = Declare.CInfo.make ~name:na ~typ:gls_type () in
+ let lemma = Declare.Proof.start ~cinfo ~info sigma in
let lemma =
if Indfun_common.is_strict_tcc () then
fst @@ Declare.Proof.by (Proofview.V82.tactic tclIDTAC) lemma
@@ -1530,12 +1528,13 @@ let com_terminate interactive_proof tcc_lemma_name tcc_lemma_ref is_mes
fonctional_ref input_type relation rec_arg_num thm_name using_lemmas nb_args
ctx hook =
let start_proof env ctx tac_start tac_end =
- let info = Declare.Info.make ~hook () in
- let lemma =
- Declare.Proof.start ~name:thm_name ~poly:false (*FIXME*) ~info ctx
- ~impargs:[]
- (EConstr.of_constr (compute_terminate_type nb_args fonctional_ref))
+ let cinfo =
+ Declare.CInfo.make ~name:thm_name
+ ~typ:(EConstr.of_constr (compute_terminate_type nb_args fonctional_ref))
+ ()
in
+ let info = Declare.Info.make ~hook () in
+ let lemma = Declare.Proof.start ~cinfo ~info ctx in
let lemma =
fst
@@ Declare.Proof.by
@@ -1605,10 +1604,12 @@ let com_eqn uctx nb_arg eq_name functional_ref f_ref terminate_ref
let f_constr = constr_of_monomorphic_global f_ref in
let equation_lemma_type = subst1 f_constr equation_lemma_type in
let info = Declare.Info.make () in
- let lemma =
- Declare.Proof.start ~name:eq_name ~poly:false evd ~info ~impargs:[]
- (EConstr.of_constr equation_lemma_type)
+ let cinfo =
+ Declare.CInfo.make ~name:eq_name
+ ~typ:(EConstr.of_constr equation_lemma_type)
+ ()
in
+ let lemma = Declare.Proof.start ~cinfo evd ~info in
let lemma =
fst
@@ Declare.Proof.by
diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml
index 405fe7b844..f16d0717df 100644
--- a/plugins/ltac/rewrite.ml
+++ b/plugins/ltac/rewrite.ml
@@ -1902,9 +1902,10 @@ 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, Locality.Global Locality.ImportDefaultBehavior in
let impargs, udecl = [], UState.default_univ_decl in
- let info = Declare.CInfo.make ~scope ~kind ~opaque ~impargs ~udecl ~poly () in
+ let cinfo = Declare.CInfo.make ~name ~impargs ~typ:types () in
+ let info = Declare.Info.make ~scope ~kind ~udecl ~poly () in
let _r : GlobRef.t =
- Declare.declare_definition ~name ~info ~types ~body sigma
+ Declare.declare_definition ~cinfo ~info ~opaque ~body sigma
in ()
let build_morphism_signature env sigma m =
@@ -1997,10 +1998,11 @@ let add_morphism_interactive atts m n : Declare.Proof.t =
| _ -> assert false
in
let hook = Declare.Hook.make hook in
- let info = Declare.Info.make ~hook ~kind () in
Flags.silently
(fun () ->
- let lemma = Declare.Proof.start ~name:instance_id ~poly ~info ~impargs:[] evd morph in
+ let cinfo = Declare.CInfo.make ~name:instance_id ~typ:morph () in
+ let info = Declare.Info.make ~poly ~hook ~kind () in
+ let lemma = Declare.Proof.start ~cinfo ~info evd in
fst (Declare.Proof.by (Tacinterp.interp tac) lemma)) ()
let add_morphism atts binders m s n =
diff --git a/stm/stm.ml b/stm/stm.ml
index 800115ce42..7af0ace215 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -1047,9 +1047,9 @@ end = struct (* {{{ *)
end (* }}} *)
(* Wrapper for the proof-closing special path for Qed *)
-let stm_qed_delay_proof ?route ~proof ~info ~id ~st ~loc ~control pending : Vernacstate.t =
+let stm_qed_delay_proof ?route ~proof ~pinfo ~id ~st ~loc ~control pending : Vernacstate.t =
set_id_for_feedback ?route dummy_doc id;
- Vernacinterp.interp_qed_delayed_proof ~proof ~info ~st ~control (CAst.make ?loc pending)
+ Vernacinterp.interp_qed_delayed_proof ~proof ~pinfo ~st ~control (CAst.make ?loc pending)
(* Wrapper for Vernacentries.interp to set the feedback id *)
(* It is currently called 19 times, this number should be certainly
@@ -1526,8 +1526,9 @@ end = struct (* {{{ *)
let opaque = Opaque in
try
let _pstate =
+ let pinfo = Declare.Proof.Proof_info.default () in
stm_qed_delay_proof ~st ~id:stop
- ~proof:pobject ~info:(Declare.Info.make ()) ~loc ~control:[] (Proved (opaque,None)) in
+ ~proof:pobject ~pinfo ~loc ~control:[] (Proved (opaque,None)) in
()
with exn ->
(* If [stm_qed_delay_proof] fails above we need to use the
@@ -1673,7 +1674,7 @@ end = struct (* {{{ *)
let proof, _info =
PG_compat.close_proof ~opaque ~keep_body_ucst_separate:true in
- let info = Declare.Info.make () in
+ let pinfo = Declare.Proof.Proof_info.default () in
(* We jump at the beginning since the kernel handles side effects by also
* looking at the ones that happen to be present in the current env *)
@@ -1686,7 +1687,7 @@ end = struct (* {{{ *)
*)
(* STATE We use the state resulting from reaching start. *)
let st = Vernacstate.freeze_interp_state ~marshallable:false in
- ignore(stm_qed_delay_proof ~id:stop ~st ~proof ~info ~loc ~control:[] (Proved (opaque,None)));
+ ignore(stm_qed_delay_proof ~id:stop ~st ~proof ~pinfo ~loc ~control:[] (Proved (opaque,None)));
(* Is this name the same than the one in scope? *)
let name = Declare.get_po_name proof in
`OK name
@@ -2497,13 +2498,13 @@ let known_state ~doc ?(redefine_qed=false) ~cache id =
| VtKeepDefined ->
CErrors.anomaly (Pp.str "Cannot delegate transparent proofs, this is a bug in the STM.")
in
- let proof, info =
+ let proof, pinfo =
PG_compat.close_future_proof ~feedback_id:id fp in
if not delegate then ignore(Future.compute fp);
reach view.next;
let st = Vernacstate.freeze_interp_state ~marshallable:false in
let control, pe = extract_pe x in
- ignore(stm_qed_delay_proof ~id ~st ~proof ~info ~loc ~control pe);
+ ignore(stm_qed_delay_proof ~id ~st ~proof ~pinfo ~loc ~control pe);
feedback ~id:id Incomplete
| { VCS.kind = `Master }, _ -> assert false
end;
@@ -2542,9 +2543,9 @@ let known_state ~doc ?(redefine_qed=false) ~cache id =
let st = Vernacstate.freeze_interp_state ~marshallable:false in
let _st = match proof with
| None -> stm_vernac_interp id st x
- | Some (proof, info) ->
+ | Some (proof, pinfo) ->
let control, pe = extract_pe x in
- stm_qed_delay_proof ~id ~st ~proof ~info ~loc ~control pe
+ stm_qed_delay_proof ~id ~st ~proof ~pinfo ~loc ~control pe
in
let wall_clock3 = Unix.gettimeofday () in
Aux_file.record_in_aux_at ?loc:x.expr.CAst.loc "proof_check_time"
diff --git a/vernac/classes.ml b/vernac/classes.ml
index c8208cd444..94040a9cef 100644
--- a/vernac/classes.ml
+++ b/vernac/classes.ml
@@ -314,8 +314,9 @@ let instance_hook info global ?hook cst =
let declare_instance_constant iinfo global impargs ?hook name udecl poly sigma term termtype =
let kind = Decls.(IsDefinition Instance) in
let scope = Locality.Global Locality.ImportDefaultBehavior in
- 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
+ let cinfo = Declare.CInfo.make ~name ~impargs ~typ:(Some termtype) () in
+ let info = Declare.Info.make ~kind ~scope ~poly ~udecl () in
+ let kn = Declare.declare_definition ~cinfo ~info ~opaque:false ~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 =
@@ -359,11 +360,12 @@ let declare_instance_open sigma ?hook ~tac ~global ~poly id pri impargs udecl id
let sigma = Evd.reset_future_goals sigma in
let kind = Decls.(IsDefinition Instance) in
let hook = Declare.Hook.(make (fun { S.dref ; _ } -> instance_hook pri global ?hook dref)) in
- let info = Declare.Info.make ~hook ~kind ~udecl () in
+ let info = Declare.Info.make ~hook ~kind ~udecl ~poly () 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 = Declare.Proof.start ~name:id ~poly ~info ~impargs sigma termtype in
+ let cinfo = Declare.CInfo.make ~name:id ~impargs ~typ:termtype () in
+ let lemma = Declare.Proof.start ~cinfo ~info sigma in
(* spiwack: I don't know what to do with the status here. *)
let lemma =
match term with
diff --git a/vernac/comDefinition.ml b/vernac/comDefinition.ml
index c89de88e95..d5ab9f03be 100644
--- a/vernac/comDefinition.ml
+++ b/vernac/comDefinition.ml
@@ -116,9 +116,10 @@ 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 cinfo = Declare.CInfo.make ~name ~impargs ~typ:types () in
+ let info = Declare.Info.make ~scope ~kind ?hook ~udecl ~poly () in
let _ : Names.GlobRef.t =
- Declare.declare_definition ~name ~info ~types ~body evd
+ Declare.declare_definition ~info ~cinfo ~opaque:false ~body evd
in ()
let do_definition_program ?hook ~name ~scope ~poly ~kind udecl bl red_option c ctypopt =
diff --git a/vernac/comFixpoint.ml b/vernac/comFixpoint.ml
index 304df6fe93..0f34adf1c7 100644
--- a/vernac/comFixpoint.ml
+++ b/vernac/comFixpoint.ml
@@ -257,11 +257,9 @@ let build_recthms ~indexes fixnames fixtypes fiximps =
in
let thms =
List.map3 (fun name typ (ctx,impargs,_) ->
- { Declare.Recthm.name
- ; typ
- ; args = List.map Context.Rel.Declaration.get_name ctx
- ; impargs})
- fixnames fixtypes fiximps
+ let args = List.map Context.Rel.Declaration.get_name ctx in
+ Declare.CInfo.make ~name ~typ ~args ~impargs ()
+ ) fixnames fixtypes fiximps
in
fix_kind, cofix, thms
@@ -270,9 +268,10 @@ let declare_fixpoint_interactive_generic ?indexes ~scope ~poly ((fixnames,_fixrs
let indexes = Option.default [] indexes in
let init_terms = Some fixdefs in
let evd = Evd.from_ctx ctx in
+ let info = Declare.Info.make ~poly ~scope ~kind:(Decls.IsDefinition fix_kind) ~udecl () in
let lemma =
- Declare.Proof.start_mutual_with_initialization ~poly ~scope ~kind:(Decls.IsDefinition fix_kind) ~udecl
- evd ~mutual_info:(cofix,indexes,init_terms) thms None in
+ Declare.Proof.start_mutual_with_initialization ~info
+ evd ~mutual_info:(cofix,indexes,init_terms) ~cinfo:thms None in
(* Declare notations *)
List.iter (Metasyntax.add_notation_interpretation (Global.env())) ntns;
lemma
@@ -283,11 +282,11 @@ 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 info = Declare.Info.make ~scope ~kind:fix_kind ~poly ~udecl () in
+ let cinfo = fixitems in
let _ : GlobRef.t list =
- Declare.declare_mutually_recursive ~info ~uctx
+ Declare.declare_mutually_recursive ~cinfo ~info ~opaque:false ~uctx
~possible_indexes:indexes ~ntns ~rec_declaration
- fixitems
in
()
diff --git a/vernac/comProgramFixpoint.ml b/vernac/comProgramFixpoint.ml
index e51a786cb0..87aa5d9b2d 100644
--- a/vernac/comProgramFixpoint.ml
+++ b/vernac/comProgramFixpoint.ml
@@ -290,7 +290,8 @@ let do_program_recursive ~scope ~poly fixkind fixl =
let evars, _, def, typ =
RetrieveObl.retrieve_obligations env name evm
(List.length rec_sign) def typ in
- ({ Declare.Recthm.name; typ; impargs; args = [] }, def, evars)
+ let cinfo = Declare.CInfo.make ~name ~typ ~impargs () in
+ (cinfo, def, evars)
in
let (fixnames,fixrs,fixdefs,fixtypes) = fix in
let fiximps = List.map pi2 info in
diff --git a/vernac/declare.ml b/vernac/declare.ml
index 0533689e01..942aa21012 100644
--- a/vernac/declare.ml
+++ b/vernac/declare.ml
@@ -66,63 +66,83 @@ module Proof_ending = struct
end
-type lemma_possible_guards = int list list
-
-module Recthm = struct
+module CInfo = struct
type 'constr t =
- { name : Names.Id.t
+ { name : Id.t
(** Name of theorem *)
; typ : 'constr
(** Type of theorem *)
- ; args : Names.Name.t list
+ ; args : Name.t list
(** Names to pre-introduce *)
; impargs : Impargs.manual_implicits
(** Explicitily declared implicit arguments *)
}
+
+ let make ~name ~typ ?(args=[]) ?(impargs=[]) () =
+ { name; typ; args; impargs }
+
let to_constr sigma thm = { thm with typ = EConstr.to_constr sigma thm.typ }
+ let get_typ { typ; _ } = typ
+ let get_name { name; _ } = name
+
end
+(** Information for a declaration, interactive or not, includes
+ parameters shared by mutual constants *)
module Info = struct
type t =
- { hook : Hook.t option
+ { poly : bool
+ ; inline : bool
+ ; kind : Decls.logical_kind
+ ; udecl : UState.universe_decl
+ ; scope : Locality.locality
+ ; hook : Hook.t option
+ }
+
+ (** Note that [opaque] doesn't appear here as it is not known at the
+ start of the proof in the interactive case. *)
+ let make ?(poly=false) ?(inline=false) ?(kind=Decls.(IsDefinition Definition))
+ ?(udecl=UState.default_univ_decl) ?(scope=Locality.Global Locality.ImportDefaultBehavior)
+ ?hook () =
+ { poly; inline; kind; udecl; scope; hook }
+
+end
+
+type lemma_possible_guards = int list list
+
+module Proof_info = struct
+
+ type t =
+ { cinfo : Constr.t CInfo.t list
+ (** cinfo contains each individual constant info in a mutual decl *)
+ ; info : Info.t
; proof_ending : Proof_ending.t CEphemeron.key
(* This could be improved and the CEphemeron removed *)
- ; scope : Locality.locality
- ; kind : Decls.logical_kind
- ; udecl: UState.universe_decl
- (** Initial universe declarations *)
- ; thms : Constr.t Recthm.t list
- (** thms contains each individual constant info in a mutual decl *)
; compute_guard : lemma_possible_guards
(** thms and compute guard are specific only to
- start_lemma_with_initialization + regular terminator *)
+ start_lemma_with_initialization + regular terminator, so we
+ could make this per-proof kind *)
}
- let make ?hook ?(proof_ending=Proof_ending.Regular) ?(scope=Locality.Global Locality.ImportDefaultBehavior)
- ?(kind=Decls.(IsProof Lemma)) ?(udecl=UState.default_univ_decl) () =
- { hook
- ; compute_guard = []
+ let make ~cinfo ~info ?(compute_guard=[]) ?(proof_ending=Proof_ending.Regular) () =
+ { cinfo
+ ; info
+ ; compute_guard
; proof_ending = CEphemeron.create proof_ending
- ; thms = []
- ; scope
- ; kind
- ; udecl
}
(* This is used due to a deficiency on the API, should fix *)
- let add_first_thm ~info ~name ~typ ~impargs =
- let thms =
- { Recthm.name
- ; impargs
- ; typ = EConstr.Unsafe.to_constr typ
- ; args = [] } :: info.thms
- in
- { info with thms }
+ let add_first_thm ~pinfo ~name ~typ ~impargs =
+ let cinfo : Constr.t CInfo.t = CInfo.make ~name ~impargs ~typ:(EConstr.Unsafe.to_constr typ) () in
+ { pinfo with cinfo = cinfo :: pinfo.cinfo }
+ (* This is called by the STM, and we have to fixup cinfo later as
+ indeed it will not be correct *)
+ let default () = make ~cinfo:[] ~info:(Info.make ()) ()
end
type t =
@@ -131,7 +151,7 @@ type t =
; proof : Proof.t
; initial_euctx : UState.t
(** The initial universe context (for the statement) *)
- ; info : Info.t
+ ; pinfo : Proof_info.t
}
(*** Proof Global manipulation ***)
@@ -174,42 +194,46 @@ let initialize_named_context_for_proof () =
let d = if Decls.variable_opacity id then NamedDecl.drop_body d else d in
Environ.push_named_context_val d signv) sign Environ.empty_named_context_val
-(** [start_proof ~name ~udecl ~poly sigma goals] starts a proof of
- name [name] with goals [goals] (a list of pairs of environment and
- conclusion). The proof is started in the evar map [sigma] (which
- can typically contain universe constraints), and with universe
- bindings [udecl]. *)
-let start_proof_core ~name ~poly ?(impargs=[]) ?(sign=initialize_named_context_for_proof ()) ~info sigma typ =
+let start_proof_core ~name ~typ ~pinfo ?(sign=initialize_named_context_for_proof ()) sigma =
(* In ?sign, we remove the bodies of variables in the named context
marked "opaque", this is a hack tho, see #10446, and
build_constant_by_tactic uses a different method that would break
program_inference_hook *)
+ let { Proof_info.info = { Info.poly; _ }; _ } = pinfo in
let goals = [Global.env_of_context sign, typ] in
let proof = Proof.start ~name ~poly sigma goals in
let initial_euctx = Evd.evar_universe_context Proof.((data proof).sigma) in
- let info = Info.add_first_thm ~name ~typ ~impargs ~info in
{ proof
; endline_tactic = None
; section_vars = None
; initial_euctx
- ; info
+ ; pinfo
}
-let start_proof = start_proof_core ?sign:None
-
-let start_dependent_proof ~name ~poly ~info goals =
- let proof = Proof.dependent_start ~name ~poly goals in
+(** [start_proof ~info ~cinfo sigma] starts a proof of [cinfo].
+ The proof is started in the evar map [sigma] (which
+ can typically contain universe constraints) *)
+let start_proof ~info ~cinfo ?proof_ending sigma =
+ let { CInfo.name; typ; _ } = cinfo in
+ let cinfo = [{ cinfo with CInfo.typ = EConstr.Unsafe.to_constr cinfo.CInfo.typ }] in
+ let pinfo = Proof_info.make ~cinfo ~info ?proof_ending () in
+ start_proof_core ~name ~typ ~pinfo ?sign:None sigma
+
+let start_dependent_proof ~info ~name goals ~proof_ending =
+ let proof = Proof.dependent_start ~name ~poly:info.Info.poly goals in
let initial_euctx = Evd.evar_universe_context Proof.((data proof).sigma) in
+ let cinfo = [] in
+ let pinfo = Proof_info.make ~info ~cinfo ~proof_ending () in
{ proof
; endline_tactic = None
; section_vars = None
; initial_euctx
- ; info
+ ; pinfo
}
let rec_tac_initializer finite guard thms snl =
if finite then
- match List.map (fun { Recthm.name; typ } -> name, (EConstr.of_constr typ)) thms with
+ match List.map (fun { CInfo.name; typ } -> name, (EConstr.of_constr typ)) thms with
| (id,_)::l -> Tactics.mutual_cofix id l 0
| _ -> assert false
else
@@ -217,52 +241,50 @@ let rec_tac_initializer finite guard thms snl =
let nl = match snl with
| None -> List.map succ (List.map List.last guard)
| Some nl -> nl
- in match List.map2 (fun { Recthm.name; typ } n -> (name, n, (EConstr.of_constr typ))) thms nl with
+ in match List.map2 (fun { CInfo.name; typ } n -> (name, n, (EConstr.of_constr typ))) thms nl with
| (id,n,_)::l -> Tactics.mutual_fix id n l 0
| _ -> assert false
-let start_proof_with_initialization ?hook ~poly ~scope ~kind ~udecl sigma thm =
- let { Recthm.name; typ; impargs; args } = thm in
+let start_proof_with_initialization ~info ~cinfo sigma =
+ let { CInfo.name; typ; args } = cinfo in
let init_tac = Tactics.auto_intros_tac args in
- let info = Info.make ?hook ~scope ~kind ~udecl () in
- (* start_lemma has the responsibility to add (name, impargs, typ)
- to thms, once Info.t is more refined this won't be necessary *)
- let lemma = start_proof ~name ~impargs ~poly ~info sigma (EConstr.of_constr typ) in
+ let pinfo = Proof_info.make ~cinfo:[cinfo] ~info () in
+ let lemma = start_proof_core ~name ~typ:(EConstr.of_constr typ) ~pinfo ?sign:None sigma in
map_proof (fun p ->
pi1 @@ Proof.run_tactic Global.(env ()) init_tac p) lemma
type mutual_info = (bool * lemma_possible_guards * Constr.t option list option)
-let start_mutual_with_initialization ?hook ~poly ~scope ~kind ~udecl sigma ~mutual_info thms snl =
- let intro_tac { Recthm.args; _ } = Tactics.auto_intros_tac args in
+let start_mutual_with_initialization ~info ~cinfo ~mutual_info sigma snl =
+ let intro_tac { CInfo.args; _ } = Tactics.auto_intros_tac args in
let init_tac, compute_guard =
let (finite,guard,init_terms) = mutual_info in
- let rec_tac = rec_tac_initializer finite guard thms snl in
+ let rec_tac = rec_tac_initializer finite guard cinfo snl in
let term_tac =
match init_terms with
| None ->
- List.map intro_tac thms
+ List.map intro_tac cinfo
| Some init_terms ->
(* This is the case for hybrid proof mode / definition
fixpoint, where terms for some constants are given with := *)
let tacl = List.map (Option.cata (EConstr.of_constr %> Tactics.exact_no_check) Tacticals.New.tclIDTAC) init_terms in
- List.map2 (fun tac thm -> Tacticals.New.tclTHEN tac (intro_tac thm)) tacl thms
+ List.map2 (fun tac thm -> Tacticals.New.tclTHEN tac (intro_tac thm)) tacl cinfo
in
Tacticals.New.tclTHENS rec_tac term_tac, guard
in
- match thms with
+ match cinfo with
| [] -> CErrors.anomaly (Pp.str "No proof to start.")
- | { Recthm.name; typ; impargs; _} :: thms ->
- let info = Info.make ?hook ~scope ~kind ~udecl () in
- let info = { info with Info.compute_guard; thms } in
+ | { CInfo.name; typ; impargs; _} :: thms ->
+ let pinfo = Proof_info.make ~cinfo ~info ~compute_guard () in
(* start_lemma has the responsibility to add (name, impargs, typ)
to thms, once Info.t is more refined this won't be necessary *)
- let lemma = start_proof ~name ~impargs ~poly ~info sigma (EConstr.of_constr typ) in
+ let typ = EConstr.of_constr typ in
+ let lemma = start_proof_core ~name ~typ ~pinfo sigma in
map_proof (fun p ->
pi1 @@ Proof.run_tactic Global.(env ()) init_tac p) lemma
let get_used_variables pf = pf.section_vars
-let get_universe_decl pf = pf.info.Info.udecl
+let get_universe_decl pf = pf.pinfo.Proof_info.info.Info.udecl
let set_used_variables ps l =
let open Context.Named.Declaration in
@@ -415,7 +437,8 @@ let make_univs ~poly ~uctx ~udecl (used_univs_typ, typ) (used_univs_body, body)
let close_proof ~opaque ~keep_body_ucst_separate ps =
- let { section_vars; proof; initial_euctx; info = { Info.udecl } } = ps in
+ let { section_vars; proof; initial_euctx; pinfo } = ps in
+ let { Proof_info.info = { Info.udecl } } = pinfo in
let { Proof.name; poly } = Proof.data proof in
let unsafe_typ = keep_body_ucst_separate && not poly in
let elist, uctx = prepare_proof ~unsafe_typ ps in
@@ -865,7 +888,8 @@ end
type closed_proof_output = (Constr.t * Evd.side_effects) list * UState.t
let close_proof_delayed ~feedback_id ps (fpl : closed_proof_output Future.computation) =
- let { section_vars; proof; initial_euctx; info = { Info.udecl } } = ps in
+ let { section_vars; proof; initial_euctx; pinfo } = ps in
+ let { Proof_info.info = { Info.udecl } } = pinfo in
let { Proof.name; poly; entry; sigma } = Proof.data proof in
(* We don't allow poly = true in this path *)
@@ -933,10 +957,13 @@ let next = let n = ref 0 in fun () -> incr n; !n
let by tac = map_fold_proof (Proof.solve (Goal_select.SelectNth 1) None tac)
-let build_constant_by_tactic ~name ?(opaque=Vernacexpr.Transparent) ~uctx ~sign ~poly typ tac =
+let build_constant_by_tactic ~name ?(opaque=Vernacexpr.Transparent) ~uctx ~sign ~poly (typ : EConstr.t) tac =
let evd = Evd.from_ctx uctx in
- let info = Info.make () in
- let pf = start_proof_core ~name ~poly ~sign ~impargs:[] ~info evd typ in
+ let typ_ = EConstr.Unsafe.to_constr typ in
+ let cinfo = [CInfo.make ~name ~typ:typ_ ()] in
+ let info = Info.make ~poly () in
+ let pinfo = Proof_info.make ~cinfo ~info () in
+ let pf = start_proof_core ~name ~typ ~pinfo ~sign evd in
let pf, status = by tac pf in
let { entries; uctx } = close_proof ~opaque ~keep_body_ucst_separate:false pf in
match entries with
@@ -1045,26 +1072,6 @@ let declare_definition_scheme ~internal ~univs ~role ~name c =
let _ = Ind_tables.declare_definition_scheme := declare_definition_scheme
let _ = Abstract.declare_abstract := declare_abstract
-module CInfo = struct
-
- type t =
- { poly : bool
- ; opaque : bool
- ; inline : bool
- ; kind : Decls.logical_kind
- ; udecl : UState.universe_decl
- ; scope : Locality.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=Locality.Global Locality.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 =
@@ -1105,10 +1112,10 @@ 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 ~info ~ntns ~uctx ~rec_declaration ~possible_indexes ?(restrict_ucontext=true) fixitems =
- let { CInfo.poly; udecl; opaque; scope; kind; _ } = info in
+let declare_mutually_recursive_core ~info ~cinfo ~opaque ~ntns ~uctx ~rec_declaration ~possible_indexes ?(restrict_ucontext=true) () =
+ let { Info.poly; udecl; scope; kind; _ } = info in
let vars, fixdecls, indexes =
- mutual_make_bodies ~fixitems ~rec_declaration ~possible_indexes in
+ mutual_make_bodies ~fixitems:cinfo ~rec_declaration ~possible_indexes in
let uctx, univs =
(* XXX: Obligations don't do this, this seems like a bug? *)
if restrict_ucontext
@@ -1121,18 +1128,18 @@ let declare_mutually_recursive_core ~info ~ntns ~uctx ~rec_declaration ~possible
uctx, univs
in
let csts = CList.map2
- (fun Recthm.{ name; typ; impargs } body ->
+ (fun CInfo.{ name; typ; impargs } body ->
let entry = definition_entry ~opaque ~types:typ ~univs body in
declare_entry ~name ~scope ~kind ~impargs ~uctx entry)
- fixitems fixdecls
+ cinfo fixdecls
in
let isfix = Option.has_some possible_indexes in
- let fixnames = List.map (fun { Recthm.name } -> name) fixitems in
+ let fixnames = List.map (fun { CInfo.name } -> name) cinfo in
recursive_message isfix indexes fixnames;
List.iter (Metasyntax.add_notation_interpretation (Global.env())) ntns;
csts
-let declare_mutually_recursive = declare_mutually_recursive_core ~restrict_ucontext:true
+let declare_mutually_recursive = declare_mutually_recursive_core ~restrict_ucontext:true ()
let warn_let_as_axiom =
CWarnings.create ~name:"let-as-axiom" ~category:"vernacular"
@@ -1156,21 +1163,22 @@ let declare_assumption ~name ~scope ~hook ~impargs ~uctx pe =
(* Preparing proof entries *)
-let prepare_definition ~info ~types ~body sigma =
- let { CInfo.poly; udecl; opaque; inline; _ } = info in
+let prepare_definition ~info ~opaque ~body ~typ sigma =
+ let { Info.poly; udecl; 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)
+ sigma (fun nf -> nf body, Option.map nf typ)
in
let univs = Evd.check_univ_decl ~poly sigma udecl 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 ~info ~obls ~types ~body sigma =
- let entry, uctx = prepare_definition ~info ~types ~body sigma in
- let { CInfo.scope; kind; impargs; hook; _ } = info in
+let declare_definition_core ~info ~cinfo ~opaque ~obls ~body sigma =
+ let { CInfo.name; impargs; typ; _ } = cinfo in
+ let entry, uctx = prepare_definition ~info ~opaque ~body ~typ sigma in
+ let { Info.scope; kind; hook; _ } = info in
declare_entry_core ~name ~scope ~kind ~impargs ~obls ?hook ~uctx entry
let declare_definition = declare_definition_core ~obls:[]
@@ -1225,10 +1233,10 @@ type fixpoint_kind = IsFixpoint of lident option list | IsCoFixpoint
module ProgramDecl = struct
type t =
- { prg_name : Id.t
- ; prg_info : CInfo.t
+ { prg_cinfo : constr CInfo.t
+ ; prg_info : Info.t
+ ; prg_opaque : bool
; prg_body : constr
- ; prg_type : constr
; prg_uctx : UState.t
; prg_obligations : obligations
; prg_deps : Id.t list
@@ -1239,16 +1247,16 @@ module ProgramDecl = struct
open Obligation
- let make prg_name ~info ~ntns ~reduce ~deps ~uctx ~types ~body fixkind obls =
+ let make ~info ~cinfo ~opaque ~ntns ~reduce ~deps ~uctx ~body ~fixpoint_kind obls =
let obls', body =
match body with
| None ->
assert (Int.equal (Array.length obls) 0);
- let n = Nameops.add_suffix prg_name "_obligation" in
+ let n = Nameops.add_suffix cinfo.CInfo.name "_obligation" in
( [| { obl_name = n
; obl_body = None
; obl_location = Loc.tag Evar_kinds.InternalHole
- ; obl_type = types
+ ; obl_type = cinfo.CInfo.typ
; obl_status = (false, Evar_kinds.Expand)
; obl_deps = Int.Set.empty
; obl_tac = None } |]
@@ -1267,31 +1275,31 @@ module ProgramDecl = struct
, b )
in
let prg_uctx = UState.make_flexible_nonalgebraic uctx in
- { prg_name
+ { prg_cinfo = { cinfo with CInfo.typ = reduce cinfo.CInfo.typ }
; prg_info = info
+ ; prg_opaque = opaque
; prg_body = body
- ; prg_type = reduce types
; prg_uctx
; prg_obligations = {obls = obls'; remaining = Array.length obls'}
; prg_deps = deps
- ; prg_fixkind = fixkind
+ ; prg_fixkind = fixpoint_kind
; prg_notations = ntns
; prg_reduce = reduce }
let show prg =
- let n = prg.prg_name in
+ let { CInfo.name; typ; _ } = prg.prg_cinfo in
let env = Global.env () in
let sigma = Evd.from_env env in
- Id.print n ++ spc () ++ str ":" ++ spc ()
- ++ Printer.pr_constr_env env sigma prg.prg_type
+ Id.print name ++ spc () ++ str ":" ++ spc ()
+ ++ Printer.pr_constr_env env sigma typ
++ spc () ++ str ":=" ++ fnl ()
++ Printer.pr_constr_env env sigma prg.prg_body
module Internal = struct
- let get_name prg = prg.prg_name
+ let get_name prg = prg.prg_cinfo.CInfo.name
let get_uctx prg = prg.prg_uctx
let set_uctx ~uctx prg = {prg with prg_uctx = uctx}
- let get_poly prg = prg.prg_info.CInfo.poly
+ let get_poly prg = prg.prg_info.Info.poly
let get_obligations prg = prg.prg_obligations
end
end
@@ -1370,7 +1378,7 @@ let unfold_entry cst = Hints.HintsUnfoldEntry [EvalConstRef cst]
let add_hint local prg cst =
let locality = if local then Goptions.OptLocal else Goptions.OptExport in
- Hints.add_hints ~locality [Id.to_string prg.prg_name] (unfold_entry cst)
+ Hints.add_hints ~locality [Id.to_string prg.prg_cinfo.CInfo.name] (unfold_entry cst)
(* true = hide obligations *)
let get_hide_obligations =
@@ -1380,7 +1388,7 @@ let get_hide_obligations =
~value:false
let declare_obligation prg obl ~uctx ~types ~body =
- let poly = prg.prg_info.CInfo.poly in
+ let poly = prg.prg_info.Info.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
@@ -1388,7 +1396,7 @@ let declare_obligation prg obl ~uctx ~types ~body =
| _, 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_info.CInfo.poly in
+ let poly = prg.prg_info.Info.poly in
let ctx, body, ty, args =
if not poly then shrink_body body types
else ([], body, types, [||])
@@ -1507,8 +1515,8 @@ let check_solved_obligations ~what_for : unit =
++ str "unsolved obligations" )
let map_replace k v m = ProgMap.add k (CEphemeron.create v) (ProgMap.remove k m)
-let progmap_remove pm prg = ProgMap.remove prg.prg_name pm
-let progmap_replace prg' pm = map_replace prg'.prg_name prg' pm
+let progmap_remove pm prg = ProgMap.remove prg.prg_cinfo.CInfo.name pm
+let progmap_replace prg' pm = map_replace prg'.prg_cinfo.CInfo.name prg' pm
let obligations_solved prg = Int.equal prg.prg_obligations.remaining 0
let obligations_message rem =
@@ -1586,21 +1594,22 @@ let replace_appvars subst =
let subst_prog subst prg =
if get_hide_obligations () then
( replace_appvars subst prg.prg_body
- , replace_appvars subst (* Termops.refresh_universes *) prg.prg_type )
+ , replace_appvars subst (* Termops.refresh_universes *) prg.prg_cinfo.CInfo.typ )
else
let subst' = List.map (fun (n, (_, b)) -> (n, b)) subst in
( Vars.replace_vars subst' prg.prg_body
- , Vars.replace_vars subst' (* Termops.refresh_universes *) prg.prg_type )
+ , Vars.replace_vars subst' (* Termops.refresh_universes *) prg.prg_cinfo.CInfo.typ )
let declare_definition prg =
let varsubst = obligation_substitution true prg 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
- let name, info = prg.prg_name, prg.prg_info in
+ let cinfo = { prg.prg_cinfo with CInfo.typ = types } in
+ let name, info, opaque = prg.prg_cinfo.CInfo.name, prg.prg_info, prg.prg_opaque in
let obls = List.map (fun (id, (_, c)) -> (id, c)) varsubst in
(* XXX: This is doing normalization twice *)
- let kn = declare_definition_core ~name ~info ~obls ~types ~body sigma in
+ let kn = declare_definition_core ~cinfo ~info ~obls ~body ~opaque sigma in
let pm = progmap_remove !State.prg_ref prg in
State.prg_ref := pm;
kn
@@ -1641,7 +1650,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_info.CInfo.impargs) in
+ let def = (x.prg_reduce term, r, x.prg_reduce typ, x.prg_cinfo.CInfo.impargs) in
let oblsubst = List.map (fun (id, (_, c)) -> (id, c)) oblsubst in
(def, oblsubst)
in
@@ -1659,13 +1668,13 @@ let declare_mutual_definition l =
( d :: a1
, r :: a2
, typ :: a3
- , Recthm.{name; typ; impargs; args = []} :: a4 ))
+ , CInfo.{name; typ; impargs; args = []} :: a4 ))
defs first.prg_deps ([], [], [], [])
in
let fixkind = Option.get first.prg_fixkind in
let arrrec, recvec = (Array.of_list fixtypes, Array.of_list fixdefs) in
let rvec = Array.of_list fixrs in
- let namevec = Array.of_list (List.map (fun x -> Name x.prg_name) l) in
+ let namevec = Array.of_list (List.map (fun x -> Name x.prg_cinfo.CInfo.name) l) in
let rec_declaration = (Array.map2 Context.make_annot namevec rvec, arrrec, recvec) in
let possible_indexes =
match fixkind with
@@ -1679,17 +1688,17 @@ let declare_mutual_definition l =
if fixkind != IsCoFixpoint then Decls.(IsDefinition Fixpoint)
else Decls.(IsDefinition CoFixpoint)
in
- let scope = first.prg_info.CInfo.scope in
+ let scope = first.prg_info.Info.scope in
(* Declare the recursive definitions *)
let kns =
declare_mutually_recursive_core ~info:first.prg_info ~ntns:first.prg_notations
- ~uctx:first.prg_uctx ~rec_declaration ~possible_indexes
- ~restrict_ucontext:false fixitems
+ ~uctx:first.prg_uctx ~rec_declaration ~possible_indexes ~opaque:first.prg_opaque
+ ~restrict_ucontext:false ~cinfo:fixitems ()
in
(* Only for the first constant *)
let dref = List.hd kns in
Hook.(
- call ?hook:first.prg_info.CInfo.hook {S.uctx = first.prg_uctx; obls; scope; dref});
+ call ?hook:first.prg_info.Info.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
@@ -1735,7 +1744,7 @@ let update_program_decl_on_defined prg obls num obl ~uctx rem ~auto =
if pred rem > 0 then
let deps = dependencies obls num in
if not (Int.Set.is_empty deps) then
- let _progress = auto (Some prg.prg_name) deps None in
+ let _progress = auto (Some prg.prg_cinfo.CInfo.name) deps None in
()
else ()
else ()
@@ -1764,7 +1773,7 @@ let obligation_terminator entries uctx {name; num; auto} =
| (_, status), false -> status
in
let obl = {obl with obl_status = (false, status)} in
- let poly = prg.prg_info.CInfo.poly in
+ let poly = prg.prg_info.Info.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 =
@@ -1809,7 +1818,7 @@ let obligation_admitted_terminator {name; num; auto} ctx' dref =
| _ -> ()
in
let inst, ctx' =
- if not prg.prg_info.CInfo.poly (* Not polymorphic *) then
+ if not prg.prg_info.Info.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
@@ -1837,14 +1846,14 @@ end
module MutualEntry : sig
val declare_variable
- : info:Info.t
+ : pinfo:Proof_info.t
-> uctx:UState.t
-> Entries.parameter_entry
-> Names.GlobRef.t list
val declare_mutdef
(* Common to all recthms *)
- : info:Info.t
+ : pinfo:Proof_info.t
-> uctx:UState.t
-> Evd.side_effects proof_entry
-> Names.GlobRef.t list
@@ -1871,8 +1880,9 @@ end = struct
Pp.(str "Not a proof by induction: " ++
Termops.Internal.debug_print_constr (EConstr.of_constr t) ++ str ".")
- let declare_mutdef ~uctx ~info pe i Recthm.{ name; impargs; typ; _} =
- let { Info.hook; scope; kind; compute_guard; _ } = info in
+ let declare_mutdef ~uctx ~pinfo pe i CInfo.{ name; impargs; typ; _} =
+ let { Proof_info.info; compute_guard; _ } = pinfo in
+ let { Info.hook; scope; kind; _ } = info in
(* if i = 0 , we don't touch the type; this is for compat
but not clear it is the right thing to do.
*)
@@ -1891,8 +1901,8 @@ end = struct
in
declare_entry ~name ~scope ~kind ?hook ~impargs ~uctx pe
- let declare_mutdef ~info ~uctx const =
- let pe = match info.Info.compute_guard with
+ let declare_mutdef ~pinfo ~uctx const =
+ let pe = match pinfo.Proof_info.compute_guard with
| [] ->
(* Not a recursive statement *)
const
@@ -1902,14 +1912,14 @@ end = struct
Internal.map_entry_body const
~f:(guess_decreasing env possible_indexes)
in
- List.map_i (declare_mutdef ~info ~uctx pe) 0 info.Info.thms
+ List.map_i (declare_mutdef ~pinfo ~uctx pe) 0 pinfo.Proof_info.cinfo
- let declare_variable ~info ~uctx pe =
- let { Info.scope; hook } = info in
+ let declare_variable ~pinfo ~uctx pe =
+ let { Info.scope; hook } = pinfo.Proof_info.info in
List.map_i (
- fun i { Recthm.name; typ; impargs } ->
+ fun i { CInfo.name; typ; impargs } ->
declare_assumption ~name ~scope ~hook ~impargs ~uctx pe
- ) 0 info.Info.thms
+ ) 0 pinfo.Proof_info.cinfo
end
@@ -1937,10 +1947,10 @@ let compute_proof_using_for_admitted proof typ pproofs =
Some (Environ.really_needed env (Id.Set.union ids_typ ids_def))
| _ -> None
-let finish_admitted ~info ~uctx pe =
- let cst = MutualEntry.declare_variable ~info ~uctx pe in
+let finish_admitted ~pinfo ~uctx pe =
+ let cst = MutualEntry.declare_variable ~pinfo ~uctx pe in
(* If the constant was an obligation we need to update the program map *)
- match CEphemeron.get info.Info.proof_ending with
+ match CEphemeron.get pinfo.Proof_info.proof_ending with
| Proof_ending.End_obligation oinfo ->
Obls.obligation_admitted_terminator oinfo uctx (List.hd cst)
| _ -> ()
@@ -1958,16 +1968,16 @@ let save_lemma_admitted ~proof =
let sec_vars = compute_proof_using_for_admitted proof typ pproofs in
let uctx = get_initial_euctx proof in
let univs = UState.check_univ_decl ~poly uctx udecl in
- finish_admitted ~info:proof.info ~uctx (sec_vars, (typ, univs), None)
+ finish_admitted ~pinfo:proof.pinfo ~uctx (sec_vars, (typ, univs), None)
(************************************************************************)
(* Saving a lemma-like constant *)
(************************************************************************)
-let finish_proved po info =
+let finish_proved po pinfo =
match po with
| { entries=[const]; uctx } ->
- let _r : Names.GlobRef.t list = MutualEntry.declare_mutdef ~info ~uctx const in
+ let _r : Names.GlobRef.t list = MutualEntry.declare_mutdef ~pinfo ~uctx const in
()
| _ ->
CErrors.anomaly ~label:"finish_proved" Pp.(str "close_proof returned more than one proof term")
@@ -2028,7 +2038,7 @@ let finish_proved_equations ~kind ~hook i proof_obj types sigma0 =
let finalize_proof proof_obj proof_info =
let open Proof_ending in
- match CEphemeron.default proof_info.Info.proof_ending Regular with
+ match CEphemeron.default proof_info.Proof_info.proof_ending Regular with
| Regular ->
finish_proved proof_obj proof_info
| End_obligation oinfo ->
@@ -2036,7 +2046,7 @@ let finalize_proof proof_obj proof_info =
| End_derive { f ; name } ->
finish_derived ~f ~name ~entries:proof_obj.entries
| End_equations { hook; i; types; sigma } ->
- finish_proved_equations ~kind:proof_info.Info.kind ~hook i proof_obj types sigma
+ finish_proved_equations ~kind:proof_info.Proof_info.info.Info.kind ~hook i proof_obj types sigma
let err_save_forbidden_in_place_of_qed () =
CErrors.user_err (Pp.str "Cannot use Save with more than one constant or in this proof mode")
@@ -2046,24 +2056,24 @@ let process_idopt_for_save ~idopt info =
| None -> info
| Some { CAst.v = save_name } ->
(* Save foo was used; we override the info in the first theorem *)
- let thms =
- match info.Info.thms, CEphemeron.default info.Info.proof_ending Proof_ending.Regular with
- | [ { Recthm.name; _} as decl ], Proof_ending.Regular ->
- [ { decl with Recthm.name = save_name } ]
+ let cinfo =
+ match info.Proof_info.cinfo, CEphemeron.default info.Proof_info.proof_ending Proof_ending.Regular with
+ | [ { CInfo.name; _} as decl ], Proof_ending.Regular ->
+ [ { decl with CInfo.name = save_name } ]
| _ ->
err_save_forbidden_in_place_of_qed ()
- in { info with Info.thms }
+ in { info with Proof_info.cinfo }
let save_lemma_proved ~proof ~opaque ~idopt =
(* Env and sigma are just used for error printing in save_remaining_recthms *)
let proof_obj = close_proof ~opaque ~keep_body_ucst_separate:false proof in
- let proof_info = process_idopt_for_save ~idopt proof.info in
+ let proof_info = process_idopt_for_save ~idopt proof.pinfo in
finalize_proof proof_obj proof_info
(***********************************************************************)
(* Special case to close a lemma without forcing a proof *)
(***********************************************************************)
-let save_lemma_admitted_delayed ~proof ~info =
+let save_lemma_admitted_delayed ~proof ~pinfo =
let { entries; uctx } = proof in
if List.length entries <> 1 then
CErrors.user_err Pp.(str "Admitted does not support multiple statements");
@@ -2076,17 +2086,17 @@ let save_lemma_admitted_delayed ~proof ~info =
| Some typ -> typ in
let ctx = UState.univ_entry ~poly uctx in
let sec_vars = if get_keep_admitted_vars () then proof_entry_secctx else None in
- finish_admitted ~uctx ~info (sec_vars, (typ, ctx), None)
+ finish_admitted ~uctx ~pinfo (sec_vars, (typ, ctx), None)
-let save_lemma_proved_delayed ~proof ~info ~idopt =
+let save_lemma_proved_delayed ~proof ~pinfo ~idopt =
(* vio2vo calls this but with invalid info, we have to workaround
that to add the name to the info structure *)
- if CList.is_empty info.Info.thms then
+ if CList.is_empty pinfo.Proof_info.cinfo then
let name = get_po_name proof in
- let info = Info.add_first_thm ~info ~name ~typ:EConstr.mkSet ~impargs:[] in
+ let info = Proof_info.add_first_thm ~pinfo ~name ~typ:EConstr.mkSet ~impargs:[] in
finalize_proof proof info
else
- let info = process_idopt_for_save ~idopt info in
+ let info = process_idopt_for_save ~idopt pinfo in
finalize_proof proof info
module Proof = struct
@@ -2110,8 +2120,9 @@ module Proof = struct
let compact = compact_the_proof
let update_global_env = update_global_env
let get_open_goals = get_open_goals
- let info { info } = info
+ let info { pinfo } = pinfo
let get_goal_context = get_goal_context
let get_current_goal_context = get_current_goal_context
let get_current_context = get_current_context
+ module Proof_info = Proof_info
end
diff --git a/vernac/declare.mli b/vernac/declare.mli
index 84f065b134..9f19d58a5d 100644
--- a/vernac/declare.mli
+++ b/vernac/declare.mli
@@ -67,21 +67,43 @@ end
(** {2 One-go, non-interactive declaration API } *)
-(** Information for a top-level constant *)
+(** Information for a single top-level named constant *)
module CInfo : sig
+ type 'constr t
+
+ val make :
+ name : Id.t
+ -> typ:'constr
+ -> ?args:Name.t list
+ -> ?impargs:Impargs.manual_implicits
+ -> unit
+ -> 'constr t
+
+ (* Eventually we would like to remove the constr parameter *)
+ val to_constr : Evd.evar_map -> EConstr.t t -> Constr.t t
+
+ val get_typ : 'constr t -> 'constr
+ (* To be removed once obligations are merged here *)
+ val get_name : 'constr t -> Id.t
+
+end
+
+(** Information for a declaration, interactive or not, includes
+ parameters shared by mutual constants *)
+module Info : sig
type t
- val make :
- ?poly:bool
- -> ?opaque : bool
+ (** Note that [opaque] doesn't appear here as it is not known at the
+ start of the proof in the interactive case. *)
+ val make
+ : ?poly:bool
-> ?inline : bool
-> ?kind : Decls.logical_kind
(** Theorem, etc... *)
-> ?udecl : UState.universe_decl
-> ?scope : Locality.locality
(** locality *)
- -> ?impargs : Impargs.manual_implicits
-> ?hook : Hook.t
(** Callback to be executed after saving the constant *)
-> unit
@@ -96,9 +118,9 @@ end
careful not to submit open terms or evar maps with stale,
unresolved existentials *)
val declare_definition
- : name:Id.t
- -> info:CInfo.t
- -> types:EConstr.t option
+ : info:Info.t
+ -> cinfo:EConstr.t option CInfo.t
+ -> opaque:bool
-> body:EConstr.t
-> Evd.evar_map
-> GlobRef.t
@@ -112,32 +134,16 @@ val declare_assumption
-> Entries.parameter_entry
-> GlobRef.t
-module Recthm : sig
- type 'constr t =
- { name : Id.t
- (** Name of theorem *)
- ; typ : 'constr
- (** Type of theorem *)
- ; args : Name.t list
- (** Names to pre-introduce *)
- ; impargs : Impargs.manual_implicits
- (** Explicitily declared implicit arguments *)
- }
-
- (* Eventually we would like to remove the constr parameter *)
- val to_constr : Evd.evar_map -> EConstr.t t -> Constr.t t
-
-end
-
type lemma_possible_guards = int list list
val declare_mutually_recursive
- : info:CInfo.t
+ : info:Info.t
+ -> cinfo: Constr.t CInfo.t list
+ -> opaque:bool
-> ntns:Vernacexpr.decl_notation list
-> uctx:UState.t
-> rec_declaration:Constr.rec_declaration
-> possible_indexes:lemma_possible_guards option
- -> Constr.t Recthm.t list
-> Names.GlobRef.t list
(** {2 Declaration of interactive constants } *)
@@ -172,74 +178,44 @@ module Proof_ending : sig
end
-module Info : sig
- type t
- val make
- : ?hook: Hook.t
- (** Callback to be executed at the end of the proof *)
- -> ?proof_ending : Proof_ending.t
- (** Info for special constants *)
- -> ?scope : Locality.locality
- (** locality *)
- -> ?kind:Decls.logical_kind
- (** Theorem, etc... *)
- -> ?udecl:UState.universe_decl
- (** Universe declaration *)
- -> unit
- -> t
-
-end
-
(** [Declare.Proof.t] Construction of constants using interactive proofs. *)
module Proof : sig
type t
- (** [start ~name ~poly ~info sigma goals] starts a proof of
- name [name] with goals [goals] (a list of pairs of environment and
- conclusion); [poly] determines if the proof is universe
- polymorphic. The proof is started in the evar map [sigma] (which
- can typically contain universe constraints). *)
+ (** [start_proof ~info ~cinfo sigma] starts a proof of [cinfo].
+ The proof is started in the evar map [sigma] (which
+ can typically contain universe constraints) *)
val start
- : name:Names.Id.t
- -> poly:bool
- -> ?impargs:Impargs.manual_implicits
- -> info:Info.t
+ : info:Info.t
+ -> cinfo:EConstr.t CInfo.t
+ -> ?proof_ending:Proof_ending.t
-> Evd.evar_map
- -> EConstr.t
-> t
(** Like [start] except that there may be dependencies between initial goals. *)
val start_dependent
- : name:Names.Id.t
- -> poly:bool
- -> info:Info.t
+ : info:Info.t
+ -> name:Id.t
-> Proofview.telescope
+ -> proof_ending:Proof_ending.t
-> t
(** Pretty much internal, used by the Lemmavernaculars *)
val start_with_initialization
- : ?hook:Hook.t
- -> poly:bool
- -> scope:Locality.locality
- -> kind:Decls.logical_kind
- -> udecl:UState.universe_decl
+ : info:Info.t
+ -> cinfo:Constr.t CInfo.t
-> Evd.evar_map
- -> Constr.t Recthm.t
-> t
type mutual_info = (bool * lemma_possible_guards * Constr.t option list option)
(** Pretty much internal, used by mutual Lemma / Fixpoint vernaculars *)
val start_mutual_with_initialization
- : ?hook:Hook.t
- -> poly:bool
- -> scope:Locality.locality
- -> kind:Decls.logical_kind
- -> udecl:UState.universe_decl
- -> Evd.evar_map
+ : info:Info.t
+ -> cinfo:Constr.t CInfo.t list
-> mutual_info:mutual_info
- -> Constr.t Recthm.t list
+ -> Evd.evar_map
-> int list option
-> t
@@ -302,7 +278,12 @@ module Proof : sig
val get_current_context : t -> Evd.evar_map * Environ.env
(* Internal, don't use *)
- val info : t -> Info.t
+ module Proof_info : sig
+ type t
+ (* Make a dummy value, used in the stm *)
+ val default : unit -> t
+ end
+ val info : t -> Proof_info.t
end
(** {2 low-level, internla API, avoid using unless you have special needs } *)
@@ -402,12 +383,12 @@ val close_future_proof : feedback_id:Stateid.t -> Proof.t -> closed_proof_output
proof information so the proof won't be forced. *)
val save_lemma_admitted_delayed :
proof:proof_object
- -> info:Info.t
+ -> pinfo:Proof.Proof_info.t
-> unit
val save_lemma_proved_delayed
: proof:proof_object
- -> info:Info.t
+ -> pinfo:Proof.Proof_info.t
-> idopt:Names.lident option
-> unit
@@ -469,15 +450,15 @@ module ProgramDecl : sig
type t
val make :
- Names.Id.t
- -> info:CInfo.t
+ info:Info.t
+ -> cinfo:Constr.types CInfo.t
+ -> opaque:bool
-> ntns:Vernacexpr.decl_notation list
-> reduce:(Constr.constr -> Constr.constr)
-> deps:Names.Id.t list
-> uctx:UState.t
- -> types:Constr.types
-> body:Constr.constr option
- -> fixpoint_kind option
+ -> fixpoint_kind:fixpoint_kind option
-> RetrieveObl.obligation_info
-> t
diff --git a/vernac/obligations.ml b/vernac/obligations.ml
index 57aa79d749..0cce9581a2 100644
--- a/vernac/obligations.ml
+++ b/vernac/obligations.ml
@@ -144,9 +144,10 @@ let rec solve_obligation prg num tac =
let name = Internal.get_name prg in
Declare.Proof_ending.End_obligation {Declare.name; num; auto}
in
- let info = Declare.Info.make ~proof_ending ~scope ~kind () in
+ let cinfo = Declare.CInfo.make ~name:obl.obl_name ~typ:(EConstr.of_constr obl.obl_type) () in
let poly = Internal.get_poly prg in
- let lemma = Declare.Proof.start ~name:obl.obl_name ~poly ~impargs:[] ~info evd (EConstr.of_constr obl.obl_type) in
+ let info = Declare.Info.make ~scope ~kind ~poly () in
+ let lemma = Declare.Proof.start ~cinfo ~info ~proof_ending evd in
let lemma = fst @@ Declare.Proof.by !default_tactic lemma in
let lemma = Option.cata (fun tac -> Declare.Proof.set_endline_tactic tac lemma) lemma tac in
lemma
@@ -307,8 +308,9 @@ let add_definition ~name ?term t ~uctx ?(udecl = UState.default_univ_decl)
?(kind = Decls.(IsDefinition Definition)) ?tactic ?(reduce = reduce) ?hook
?(opaque = false) obls =
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
+ let info = Declare.Info.make ~poly ~udecl ~scope ~kind ?hook () in
+ let cinfo = Declare.CInfo.make ~name ~typ:t ~impargs () in
+ ProgramDecl.make ~info ~cinfo ~body:term ~opaque ~uctx ~reduce ~ntns:[] ~deps:[] ~fixpoint_kind:None obls
in
let {obls;_} = Internal.get_obligations prg in
if Int.equal (Array.length obls) 0 then (
@@ -329,16 +331,16 @@ let add_mutual_definitions l ~uctx ?(udecl = UState.default_univ_decl)
?tactic ~poly ?(scope = Locality.Global Locality.ImportDefaultBehavior)
?(kind = Decls.(IsDefinition Definition)) ?(reduce = reduce) ?hook ?(opaque = false)
notations fixkind =
- let deps = List.map (fun ({Declare.Recthm.name; _}, _, _) -> name) l in
+ let deps = List.map (fun (ci,_,_) -> Declare.CInfo.get_name ci) 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
+ (fun () (cinfo, b, obls) ->
+ let info = Declare.Info.make ~poly ~scope ~kind ~udecl ?hook () in
let prg =
- ProgramDecl.make name ~info ~body:(Some b) ~types:typ ~uctx ~deps
- (Some fixkind) ~ntns:notations obls ~reduce
+ ProgramDecl.make ~info ~cinfo ~opaque ~body:(Some b) ~uctx ~deps
+ ~fixpoint_kind:(Some fixkind) ~ntns:notations obls ~reduce
in
- State.add name prg)
+ State.add (Declare.CInfo.get_name cinfo) prg)
() l
in
let pm, _defined =
diff --git a/vernac/obligations.mli b/vernac/obligations.mli
index ee6a9a17bb..c7ab4a0794 100644
--- a/vernac/obligations.mli
+++ b/vernac/obligations.mli
@@ -87,7 +87,7 @@ val add_definition :
(** Start a [Program Fixpoint] declaration, similar to the above,
except it takes a list now. *)
val add_mutual_definitions :
- (Constr.t Declare.Recthm.t * Constr.t * RetrieveObl.obligation_info) list
+ (Constr.t Declare.CInfo.t * Constr.t * RetrieveObl.obligation_info) list
-> uctx:UState.t
-> ?udecl:UState.universe_decl (** Universe binders and constraints *)
-> ?tactic:unit Proofview.tactic
diff --git a/vernac/recLemmas.ml b/vernac/recLemmas.ml
index c08fdf8b96..e276918526 100644
--- a/vernac/recLemmas.ml
+++ b/vernac/recLemmas.ml
@@ -16,7 +16,8 @@ module RelDecl = Context.Rel.Declaration
let find_mutually_recursive_statements sigma thms =
let n = List.length thms in
- let inds = List.map (fun ({ Declare.Recthm.name; typ; args; impargs} as x) ->
+ let inds = List.map (fun x ->
+ let typ = Declare.CInfo.get_typ x in
let (hyps,ccl) = EConstr.decompose_prod_assum sigma typ in
let whnf_hyp_hds = EConstr.map_rel_context_in_env
(fun env c -> fst (Reductionops.whd_all_stack env sigma c))
@@ -89,10 +90,10 @@ let find_mutually_recursive_statements sigma thms =
(finite,guard,None), ordered_inds
type mutual_info =
- | NonMutual of EConstr.t Declare.Recthm.t
+ | NonMutual of EConstr.t Declare.CInfo.t
| Mutual of
{ mutual_info : Declare.Proof.mutual_info
- ; thms : EConstr.t Declare.Recthm.t list
+ ; thms : EConstr.t Declare.CInfo.t list
; possible_guards : int list
}
diff --git a/vernac/recLemmas.mli b/vernac/recLemmas.mli
index 64890962ba..a1cadd9bc1 100644
--- a/vernac/recLemmas.mli
+++ b/vernac/recLemmas.mli
@@ -9,14 +9,14 @@
(************************************************************************)
type mutual_info =
- | NonMutual of EConstr.t Declare.Recthm.t
+ | NonMutual of EConstr.t Declare.CInfo.t
| Mutual of
{ mutual_info : Declare.Proof.mutual_info
- ; thms : EConstr.t Declare.Recthm.t list
+ ; thms : EConstr.t Declare.CInfo.t list
; possible_guards : int list
}
val look_for_possibly_mutual_statements
: Evd.evar_map
- -> EConstr.t Declare.Recthm.t list
+ -> EConstr.t Declare.CInfo.t list
-> mutual_info
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index f1ffb947c1..c9d56395c2 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -503,9 +503,8 @@ let interp_lemma ~program_mode ~flags ~scope env0 evd thms =
let evd = Pretyping.solve_remaining_evars ?hook:inference_hook flags env evd in
let ids = List.map Context.Rel.Declaration.get_name ctx in
check_name_freshness scope id;
- let thm = { Declare.Recthm.name = id.CAst.v
- ; typ = EConstr.it_mkProd_or_LetIn t' ctx
- ; args = ids; impargs = imps @ imps' } in
+ let thm = Declare.CInfo.make ~name:id.CAst.v ~typ:(EConstr.it_mkProd_or_LetIn t' ctx)
+ ~args:ids ~impargs:(imps @ imps') () in
evd, thm)
evd thms
@@ -530,13 +529,15 @@ let start_lemma_com ~program_mode ~poly ~scope ~kind ?hook thms =
let evd = Evd.minimize_universes evd in
match mut_analysis with
| RecLemmas.NonMutual thm ->
- let thm = Declare.Recthm.to_constr evd thm in
+ let thm = Declare.CInfo.to_constr evd thm in
let evd = post_check_evd ~udecl ~poly evd in
- Declare.Proof.start_with_initialization ?hook ~poly ~scope ~kind evd ~udecl thm
+ let info = Declare.Info.make ?hook ~poly ~scope ~kind ~udecl () in
+ Declare.Proof.start_with_initialization ~info ~cinfo:thm evd
| RecLemmas.Mutual { mutual_info; thms ; possible_guards } ->
- let thms = List.map (Declare.Recthm.to_constr evd) thms in
+ let thms = List.map (Declare.CInfo.to_constr evd) thms in
let evd = post_check_evd ~udecl ~poly evd in
- Declare.Proof.start_mutual_with_initialization ?hook ~poly ~scope ~kind evd ~udecl ~mutual_info thms (Some possible_guards)
+ let info = Declare.Info.make ?hook ~poly ~scope ~kind ~udecl () in
+ Declare.Proof.start_mutual_with_initialization ~info ~cinfo:thms evd ~mutual_info (Some possible_guards)
let vernac_definition_hook ~canonical_instance ~local ~poly = let open Decls in function
| Coercion ->
diff --git a/vernac/vernacinterp.ml b/vernac/vernacinterp.ml
index 09cb9e4c8c..3e7101834f 100644
--- a/vernac/vernacinterp.ml
+++ b/vernac/vernacinterp.ml
@@ -213,21 +213,21 @@ and interp_control ~st ({ CAst.v = cmd } as vernac) =
*)
(* Interpreting a possibly delayed proof *)
-let interp_qed_delayed ~proof ~info ~st pe : Vernacstate.LemmaStack.t option =
+let interp_qed_delayed ~proof ~pinfo ~st pe : Vernacstate.LemmaStack.t option =
let stack = st.Vernacstate.lemmas in
let stack = Option.cata (fun stack -> snd @@ Vernacstate.LemmaStack.pop stack) None stack in
let () = match pe with
| Admitted ->
- Declare.save_lemma_admitted_delayed ~proof ~info
+ Declare.save_lemma_admitted_delayed ~proof ~pinfo
| Proved (_,idopt) ->
- Declare.save_lemma_proved_delayed ~proof ~info ~idopt in
+ Declare.save_lemma_proved_delayed ~proof ~pinfo ~idopt in
stack
-let interp_qed_delayed_control ~proof ~info ~st ~control { CAst.loc; v=pe } =
+let interp_qed_delayed_control ~proof ~pinfo ~st ~control { CAst.loc; v=pe } =
let time_header = mk_time_header (CAst.make ?loc { control; attrs = []; expr = VernacEndProof pe }) in
List.fold_right (fun flag fn -> interp_control_flag ~time_header flag fn)
control
- (fun ~st -> interp_qed_delayed ~proof ~info ~st pe)
+ (fun ~st -> interp_qed_delayed ~proof ~pinfo ~st pe)
~st
(* General interp with management of state *)
@@ -257,6 +257,6 @@ let interp_gen ~verbosely ~st ~interp_fn cmd =
let interp ?(verbosely=true) ~st cmd =
interp_gen ~verbosely ~st ~interp_fn:interp_control cmd
-let interp_qed_delayed_proof ~proof ~info ~st ~control pe : Vernacstate.t =
+let interp_qed_delayed_proof ~proof ~pinfo ~st ~control pe : Vernacstate.t =
interp_gen ~verbosely:false ~st
- ~interp_fn:(interp_qed_delayed_control ~proof ~info ~control) pe
+ ~interp_fn:(interp_qed_delayed_control ~proof ~pinfo ~control) pe
diff --git a/vernac/vernacinterp.mli b/vernac/vernacinterp.mli
index 675dfd11f3..35ae4f2296 100644
--- a/vernac/vernacinterp.mli
+++ b/vernac/vernacinterp.mli
@@ -15,7 +15,7 @@ val interp : ?verbosely:bool -> st:Vernacstate.t -> Vernacexpr.vernac_control ->
proof and won't be forced *)
val interp_qed_delayed_proof
: proof:Declare.proof_object
- -> info:Declare.Info.t
+ -> pinfo:Declare.Proof.Proof_info.t
-> st:Vernacstate.t
-> control:Vernacexpr.control_flag list
-> Vernacexpr.proof_end CAst.t
diff --git a/vernac/vernacstate.ml b/vernac/vernacstate.ml
index 2a5762b712..cb45dc9e15 100644
--- a/vernac/vernacstate.ml
+++ b/vernac/vernacstate.ml
@@ -152,8 +152,7 @@ module Declare = struct
s_lemmas := Some stack;
res
- type closed_proof = Declare.proof_object * Declare.Info.t
-
+ type closed_proof = Declare.proof_object * Declare.Proof.Proof_info.t
let return_proof () = cc Declare.return_proof
let return_partial_proof () = cc Declare.return_partial_proof
diff --git a/vernac/vernacstate.mli b/vernac/vernacstate.mli
index 62afdb92ff..343c8d0fe3 100644
--- a/vernac/vernacstate.mli
+++ b/vernac/vernacstate.mli
@@ -68,7 +68,7 @@ module Declare : sig
val return_proof : unit -> Declare.closed_proof_output
val return_partial_proof : unit -> Declare.closed_proof_output
- type closed_proof = Declare.proof_object * Declare.Info.t
+ type closed_proof = Declare.proof_object * Declare.Proof.Proof_info.t
val close_future_proof :
feedback_id:Stateid.t ->
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 10:13:12 +0000