aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--proofs/pfedit.ml2
-rw-r--r--proofs/proof_global.ml8
-rw-r--r--proofs/proof_global.mli4
-rw-r--r--stm/stm.ml4
-rw-r--r--vernac/classes.ml4
-rw-r--r--vernac/comFixpoint.ml12
-rw-r--r--vernac/lemmas.ml131
-rw-r--r--vernac/lemmas.mli34
-rw-r--r--vernac/vernacentries.mli2
-rw-r--r--vernac/vernacstate.ml2
-rw-r--r--vernac/vernacstate.mli2
11 files changed, 122 insertions, 83 deletions
diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml
index cb4eabcc85..d00f2c4803 100644
--- a/proofs/pfedit.ml
+++ b/proofs/pfedit.ml
@@ -119,7 +119,7 @@ let next = let n = ref 0 in fun () -> incr n; !n
let build_constant_by_tactic id ctx sign ?(goal_kind = Global ImportDefaultBehavior, false, Proof Theorem) typ tac =
let evd = Evd.from_ctx ctx in
let goals = [ (Global.env_of_context sign , typ) ] in
- let pf = Proof_global.start_proof evd id goal_kind goals in
+ let pf = Proof_global.start_proof evd id UState.default_univ_decl goal_kind goals in
try
let pf, status = by tac pf in
let open Proof_global in
diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml
index 4490fbdd64..dfd54594eb 100644
--- a/proofs/proof_global.ml
+++ b/proofs/proof_global.ml
@@ -91,19 +91,19 @@ let set_endline_tactic tac ps =
end of the proof to close the proof. The proof is started in the
evar map [sigma] (which can typically contain universe
constraints), and with universe bindings pl. *)
-let start_proof sigma name ?(pl=UState.default_univ_decl) kind goals =
+let start_proof sigma name udecl kind goals =
{ proof = Proof.start ~name ~poly:(pi2 kind) sigma goals
; endline_tactic = None
; section_vars = None
- ; universe_decl = pl
+ ; universe_decl = udecl
; strength = kind
}
-let start_dependent_proof name ?(pl=UState.default_univ_decl) kind goals =
+let start_dependent_proof name udecl kind goals =
{ proof = Proof.dependent_start ~name ~poly:(pi2 kind) goals
; endline_tactic = None
; section_vars = None
- ; universe_decl = pl
+ ; universe_decl = udecl
; strength = kind
}
diff --git a/proofs/proof_global.mli b/proofs/proof_global.mli
index 4e1aa64e7b..17f5c73560 100644
--- a/proofs/proof_global.mli
+++ b/proofs/proof_global.mli
@@ -63,7 +63,7 @@ type opacity_flag = Opaque | Transparent
val start_proof
: Evd.evar_map
-> Names.Id.t
- -> ?pl:UState.universe_decl
+ -> UState.universe_decl
-> Decl_kinds.goal_kind
-> (Environ.env * EConstr.types) list
-> t
@@ -72,7 +72,7 @@ val start_proof
initial goals. *)
val start_dependent_proof
: Names.Id.t
- -> ?pl:UState.universe_decl
+ -> UState.universe_decl
-> Decl_kinds.goal_kind
-> Proofview.telescope
-> t
diff --git a/stm/stm.ml b/stm/stm.ml
index 89d95d0cc9..2fefb7fbb3 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -1537,7 +1537,7 @@ end = struct (* {{{ *)
let st = Vernacstate.freeze_interp_state ~marshallable:false in
stm_vernac_interp stop
- ~proof:(pobject, Lemmas.default_info) st
+ ~proof:(pobject, Lemmas.default_lemma_info) st
{ verbose = false; indentation = 0; strlen = 0;
expr = CAst.make ?loc @@ VernacExpr ([], VernacEndProof (Proved (opaque,None))) }) in
ignore(Future.join checked_proof);
@@ -1677,7 +1677,7 @@ end = struct (* {{{ *)
let pterm, _info =
PG_compat.close_proof ~opaque ~keep_body_ucst_separate:true (fun x -> x) in
- let proof = pterm, Lemmas.default_info in
+ let proof = pterm, Lemmas.default_lemma_info 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 *)
diff --git a/vernac/classes.ml b/vernac/classes.ml
index d6a2f2727a..b8eb7e2ab1 100644
--- a/vernac/classes.ml
+++ b/vernac/classes.ml
@@ -366,7 +366,7 @@ let declare_instance_program env sigma ~global ~poly id pri imps decl term termt
~univdecl:decl typ ctx ~kind:(Global ImportDefaultBehavior,poly,Instance) ~hook obls)
-let declare_instance_open sigma ?hook ~tac ~global ~poly id pri imps decl ids term termtype =
+let declare_instance_open sigma ?hook ~tac ~global ~poly id pri imps udecl ids term termtype =
(* spiwack: it is hard to reorder the actions to do
the pretyping after the proof has opened. As a
consequence, we use the low-level primitives to code
@@ -374,7 +374,7 @@ let declare_instance_open sigma ?hook ~tac ~global ~poly id pri imps decl ids te
let gls = List.rev (Evd.future_goals sigma) in
let sigma = Evd.reset_future_goals sigma in
let kind = Decl_kinds.(Global ImportDefaultBehavior, poly, DefinitionBody Instance) in
- let lemma = Lemmas.start_lemma id ~pl:decl kind sigma (EConstr.of_constr termtype)
+ let lemma = Lemmas.start_lemma id ~udecl kind sigma (EConstr.of_constr termtype)
~hook:(DeclareDef.Hook.make
(fun _ _ _ -> instance_hook pri global imps ?hook)) in
(* spiwack: I don't know what to do with the status here. *)
diff --git a/vernac/comFixpoint.ml b/vernac/comFixpoint.ml
index a88413cf7f..d5fb2a140c 100644
--- a/vernac/comFixpoint.ml
+++ b/vernac/comFixpoint.ml
@@ -261,8 +261,10 @@ let declare_fixpoint_notations ntns =
let declare_fixpoint_interactive local poly ((fixnames,fixrs,fixdefs,fixtypes),pl,ctx,fiximps) indexes ntns =
(* Some bodies to define by proof *)
let thms =
- List.map3 (fun id t (ctx,imps,_) -> (id,(EConstr.of_constr t,(List.map RelDecl.get_name ctx,imps))))
- fixnames fixtypes fiximps in
+ List.map3 (fun name t (ctx,impargs,_) ->
+ { Lemmas.Recthm.name; typ = EConstr.of_constr t
+ ; args = List.map RelDecl.get_name ctx; impargs})
+ fixnames fixtypes fiximps in
let init_tac =
Some (List.map (Option.cata (EConstr.of_constr %> Tactics.exact_no_check) Tacticals.New.tclIDTAC)
fixdefs) in
@@ -299,8 +301,10 @@ let declare_cofixpoint_notations = declare_fixpoint_notations
let declare_cofixpoint_interactive local poly ((fixnames,fixrs,fixdefs,fixtypes),pl,ctx,fiximps) ntns =
(* Some bodies to define by proof *)
let thms =
- List.map3 (fun id t (ctx,imps,_) -> (id,(EConstr.of_constr t,(List.map RelDecl.get_name ctx,imps))))
- fixnames fixtypes fiximps in
+ List.map3 (fun name t (ctx,impargs,_) ->
+ { Lemmas.Recthm.name; typ = EConstr.of_constr t
+ ; args = List.map RelDecl.get_name ctx; impargs})
+ fixnames fixtypes fiximps in
let init_tac =
Some (List.map (Option.cata (EConstr.of_constr %> Tactics.exact_no_check) Tacticals.New.tclIDTAC)
fixdefs) in
diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml
index c2de83c1bb..6a06493bfa 100644
--- a/vernac/lemmas.ml
+++ b/vernac/lemmas.ml
@@ -56,15 +56,38 @@ module Proof_ending = struct
end
-(* Proofs with a save constant function *)
-type t =
- { proof : Proof_global.t
- ; hook : DeclareDef.Hook.t option
+module Recthm = struct
+ type t =
+ { name : Id.t
+ ; typ : EConstr.t
+ ; args : Name.t list
+ ; impargs : Impargs.manual_implicits
+ }
+end
+
+type lemma_info =
+ { hook : DeclareDef.Hook.t option
; compute_guard : lemma_possible_guards
+ ; impargs : Impargs.manual_implicits
+ ; udecl : UState.universe_decl (* This is sadly not available on the save_proof path *)
; proof_ending : Proof_ending.t CEphemeron.key
(* This could be improved and the CEphemeron removed *)
}
+let default_lemma_info =
+ { hook = None
+ ; compute_guard = []
+ ; impargs = []
+ ; udecl = UState.default_univ_decl
+ ; proof_ending = CEphemeron.create Proof_ending.Regular
+ }
+
+(* Proofs with a save constant function *)
+type t =
+ { proof : Proof_global.t
+ ; info : lemma_info
+ }
+
let pf_map f pf = { pf with proof = f pf.proof }
let pf_fold f pf = f pf.proof
@@ -73,12 +96,11 @@ let set_endline_tactic t = pf_map (Proof_global.set_endline_tactic t)
(* To be removed *)
module Internal = struct
-(** Gets the current terminator without checking that the proof has
- been completed. Useful for the likes of [Admitted]. *)
-let get_info ps = ps.hook, ps.compute_guard, ps.proof_ending
+ (** Gets the current terminator without checking that the proof has
+ been completed. Useful for the likes of [Admitted]. *)
+ let get_info ps = ps.info
end
-(* Internal *)
let by tac pf =
let proof, res = Pfedit.by tac pf.proof in
@@ -221,8 +243,9 @@ let check_name_freshness locality {CAst.loc;v=id} : unit =
then
user_err ?loc (Id.print id ++ str " already exists.")
-let save_remaining_recthms env sigma (locality,p,kind) norm univs body opaq i (id,(t_i,(_,imps))) =
- let t_i = norm t_i in
+let save_remaining_recthms env sigma (locality,p,kind) norm univs body opaq i
+ { Recthm.name; typ; impargs } =
+ let t_i = norm typ in
let k = IsAssumption Conjectural in
match body with
| None ->
@@ -236,13 +259,13 @@ let save_remaining_recthms env sigma (locality,p,kind) norm univs body opaq i (i
| Monomorphic_entry univs -> univs
in
let c = SectionLocalAssum ((t_i, univs),p,impl) in
- let _ = declare_variable id (Lib.cwd(),c,k) in
- (VarRef id,imps)
+ let _ = declare_variable name (Lib.cwd(),c,k) in
+ (VarRef name,impargs)
| Global local ->
let k = IsAssumption Conjectural in
let decl = (ParameterEntry (None,(t_i,univs),None), k) in
- let kn = declare_constant id ~local decl in
- (ConstRef kn,imps))
+ let kn = declare_constant name ~local decl in
+ (ConstRef kn,impargs))
| Some body ->
let body = norm body in
let k = Kindops.logical_kind_of_goal_kind kind in
@@ -259,14 +282,14 @@ let save_remaining_recthms env sigma (locality,p,kind) norm univs body opaq i (i
| Discharge ->
let const = definition_entry ~types:t_i ~opaque:opaq ~univs body_i in
let c = SectionLocalDef const in
- let _ = declare_variable id (Lib.cwd(), c, k) in
- (VarRef id,imps)
+ let _ = declare_variable name (Lib.cwd(), c, k) in
+ (VarRef name,impargs)
| Global local ->
let const =
Declare.definition_entry ~types:t_i ~univs ~opaque:opaq body_i
in
- let kn = declare_constant id ~local (DefinitionEntry const, k) in
- (ConstRef kn,imps)
+ let kn = declare_constant name ~local (DefinitionEntry const, k) in
+ (ConstRef kn,impargs)
let initialize_named_context_for_proof () =
let sign = Global.named_context () in
@@ -312,33 +335,37 @@ module Stack = struct
end
(* Starting a goal *)
-let start_lemma id ?pl kind sigma ?(proof_ending = Proof_ending.Regular)
- ?(sign=initialize_named_context_for_proof()) ?(compute_guard=[]) ?hook c =
+let start_lemma id ?(udecl = UState.default_univ_decl) kind sigma ?(proof_ending = Proof_ending.Regular)
+ ?(sign=initialize_named_context_for_proof()) ?(compute_guard=[]) ?hook ?(impargs=[]) c =
let goals = [ Global.env_of_context sign , c ] in
- let proof = Proof_global.start_proof sigma id ?pl kind goals in
- { proof ; hook; compute_guard; proof_ending = CEphemeron.create proof_ending }
-
-let start_dependent_lemma id ?pl kind ?(proof_ending = Proof_ending.Regular)
- ?(compute_guard=[]) ?hook telescope =
- let proof = Proof_global.start_dependent_proof id ?pl kind telescope in
- { proof; hook; compute_guard; proof_ending = CEphemeron.create proof_ending }
+ let proof = Proof_global.start_proof sigma id udecl kind goals in
+ let proof_ending = CEphemeron.create proof_ending in
+ let info = { hook; compute_guard; impargs; udecl; proof_ending } in
+ { proof ; info }
+
+let start_dependent_lemma id ?(udecl = UState.default_univ_decl) kind ?(proof_ending = Proof_ending.Regular) ?(compute_guard=[]) ?hook
+ ?(impargs=[]) telescope =
+ let proof = Proof_global.start_dependent_proof id udecl kind telescope in
+ let proof_ending = CEphemeron.create proof_ending in
+ let info = { hook; compute_guard; impargs; udecl; proof_ending } in
+ { proof; info }
let rec_tac_initializer finite guard thms snl =
if finite then
- match List.map (fun (id,(t,_)) -> (id,t)) thms with
+ match List.map (fun { Recthm.name; typ } -> name,typ) thms with
| (id,_)::l -> Tactics.mutual_cofix id l 0
| _ -> assert false
else
(* nl is dummy: it will be recomputed at Qed-time *)
- let nl = match snl with
+ let nl = match snl with
| None -> List.map succ (List.map List.last guard)
| Some nl -> nl
- in match List.map2 (fun (id,(t,_)) n -> (id,n, t)) thms nl with
+ in match List.map2 (fun { Recthm.name; typ } n -> (name, n, typ)) thms nl with
| (id,n,_)::l -> Tactics.mutual_fix id n l 0
| _ -> assert false
-let start_lemma_with_initialization ?hook kind sigma decl recguard thms snl =
- let intro_tac (_, (_, (ids, _))) = Tactics.auto_intros_tac ids in
+let start_lemma_with_initialization ?hook kind sigma udecl recguard thms snl =
+ let intro_tac { Recthm.args; _ } = Tactics.auto_intros_tac args in
let init_tac,guard = match recguard with
| Some (finite,guard,init_tac) ->
let rec_tac = rec_tac_initializer finite guard thms snl in
@@ -354,7 +381,7 @@ let start_lemma_with_initialization ?hook kind sigma decl recguard thms snl =
Some (intro_tac (List.hd thms)), [] in
match thms with
| [] -> anomaly (Pp.str "No proof to start.")
- | (id,(t,(_,imps)))::other_thms ->
+ | { Recthm.name; typ; impargs; _}::other_thms ->
let hook ctx _ strength ref =
let other_thms_data =
if List.is_empty other_thms then [] else
@@ -362,20 +389,19 @@ let start_lemma_with_initialization ?hook kind sigma decl recguard thms snl =
let body,opaq = retrieve_first_recthm ctx ref in
let norm c = EConstr.to_constr (Evd.from_ctx ctx) c in
let body = Option.map EConstr.of_constr body in
- let uctx = UState.check_univ_decl ~poly:(pi2 kind) ctx decl in
+ let uctx = UState.check_univ_decl ~poly:(pi2 kind) ctx udecl in
let env = Global.env () in
List.map_i (save_remaining_recthms env sigma kind norm uctx body opaq) 1 other_thms in
- let thms_data = (ref,imps)::other_thms_data in
+ let thms_data = (ref,impargs)::other_thms_data in
List.iter (fun (ref,imps) ->
maybe_declare_manual_implicits false ref imps;
DeclareDef.Hook.call ?hook ctx [] strength ref) thms_data in
let hook = DeclareDef.Hook.make hook in
- let lemma = start_lemma id ~pl:decl kind sigma t ~hook ~compute_guard:guard in
- let lemma = pf_map (Proof_global.map_proof (fun p ->
- match init_tac with
- | None -> p
- | Some tac -> pi1 @@ Proof.run_tactic Global.(env ()) tac p)) lemma in
- lemma
+ let lemma = start_lemma name ~impargs ~udecl kind sigma typ ~hook ~compute_guard:guard in
+ pf_map (Proof_global.map_proof (fun p ->
+ match init_tac with
+ | None -> p
+ | Some tac -> pi1 @@ Proof.run_tactic Global.(env ()) tac p)) lemma
let start_lemma_com ~program_mode ?inference_hook ?hook kind thms =
let env0 = Global.env () in
@@ -398,7 +424,8 @@ let start_lemma_com ~program_mode ?inference_hook ?hook kind thms =
let evd = Evd.minimize_universes evd in
(* XXX: This nf_evar is critical too!! We are normalizing twice if
you look at the previous lines... *)
- let thms = List.map (fun (n, (t, info)) -> (n, (nf_evar evd t, info))) thms in
+ let thms = List.map (fun (name, (typ, (args, impargs))) ->
+ { Recthm.name; typ = nf_evar evd typ; args; impargs} ) thms in
let () =
let open UState in
if not (decl.univdecl_extensible_instance && decl.univdecl_extensible_constraints) then
@@ -446,7 +473,7 @@ let get_keep_admitted_vars =
let save_lemma_admitted ?proof ~(lemma : t) =
let open Proof_global in
match proof with
- | Some ({ id; entries; persistence = k; universes }, (hook, _, _)) ->
+ | Some ({ id; entries; persistence = k; universes }, { hook; _} ) ->
if List.length entries <> 1 then
user_err Pp.(str "Admitted does not support multiple statements");
let { proof_entry_secctx; proof_entry_type } = List.hd entries in
@@ -483,18 +510,15 @@ let save_lemma_admitted ?proof ~(lemma : t) =
| _ -> None in
let decl = Proof_global.get_universe_decl lemma.proof in
let ctx = UState.check_univ_decl ~poly universes decl in
- finish_admitted name gk (sec_vars, (typ, ctx), None) universes lemma.hook
+ finish_admitted name gk (sec_vars, (typ, ctx), None) universes lemma.info.hook
(************************************************************************)
(* Saving a lemma-like constant *)
(************************************************************************)
-type proof_info = DeclareDef.Hook.t option * lemma_possible_guards * Proof_ending.t CEphemeron.key
-
-let default_info = None, [], CEphemeron.create Proof_ending.Regular
-
-let finish_proved opaque idopt po hook compute_guard =
+let finish_proved opaque idopt po info =
let open Proof_global in
+ let { hook; compute_guard; udecl; impargs } = info in
match po with
| { id; entries=[const]; persistence=locality,poly,kind; universes } ->
let is_opaque = match opaque with
@@ -615,17 +639,16 @@ let save_lemma_proved ?proof ?lemma ~opaque ~idopt =
| None ->
(* XXX: The close_proof and proof state API should be refactored
so it is possible to insert proofs properly into the state *)
- let { proof; hook; compute_guard; proof_ending } = Option.get lemma in
- Proof_global.close_proof ~opaque ~keep_body_ucst_separate:false (fun x -> x) proof, (hook, compute_guard, proof_ending)
+ let { proof; info } = Option.get lemma in
+ Proof_global.close_proof ~opaque ~keep_body_ucst_separate:false (fun x -> x) proof, info
| Some (proof, info) ->
proof, info
in
- let hook, compute_guard, proof_ending = proof_info in
let open Proof_global in
let open Proof_ending in
- match CEphemeron.default proof_ending Regular with
+ match CEphemeron.default proof_info.proof_ending Regular with
| Regular ->
- finish_proved opaque idopt proof_obj hook compute_guard
+ finish_proved opaque idopt proof_obj proof_info
| End_obligation oinfo ->
DeclareObl.obligation_terminator opaque proof_obj.entries proof_obj.universes oinfo
| End_derive { f ; name } ->
diff --git a/vernac/lemmas.mli b/vernac/lemmas.mli
index 70c8b511a1..63b1dbb75b 100644
--- a/vernac/lemmas.mli
+++ b/vernac/lemmas.mli
@@ -60,25 +60,39 @@ module Proof_ending : sig
end
+module Recthm : sig
+ type t =
+ { name : Id.t
+ (** Name of theorem *)
+ ; typ : EConstr.t
+ (** Type of theorem *)
+ ; args : Name.t list
+ (** Names to pre-introduce *)
+ ; impargs : Impargs.manual_implicits
+ }
+end
+
val start_lemma
: Id.t
- -> ?pl:UState.universe_decl
+ -> ?udecl:UState.universe_decl
-> goal_kind
-> Evd.evar_map
-> ?proof_ending:Proof_ending.t
-> ?sign:Environ.named_context_val
-> ?compute_guard:lemma_possible_guards
-> ?hook:DeclareDef.Hook.t
+ -> ?impargs:Impargs.manual_implicits
-> EConstr.types
-> t
val start_dependent_lemma
: Id.t
- -> ?pl:UState.universe_decl
+ -> ?udecl:UState.universe_decl
-> goal_kind
-> ?proof_ending:Proof_ending.t
-> ?compute_guard:lemma_possible_guards
-> ?hook:DeclareDef.Hook.t
+ -> ?impargs:Impargs.manual_implicits
-> Proofview.telescope
-> t
@@ -92,9 +106,7 @@ val start_lemma_with_initialization
: ?hook:DeclareDef.Hook.t
-> goal_kind -> Evd.evar_map -> UState.universe_decl
-> (bool * lemma_possible_guards * unit Proofview.tactic list option) option
- -> (Id.t (* name of thm *) *
- (EConstr.types (* type of thm *) *
- (Name.t list (* names to pre-introduce *) * Impargs.manual_implicits))) list
+ -> Recthm.t list
-> int list option
-> t
@@ -107,17 +119,16 @@ val initialize_named_context_for_proof : unit -> Environ.named_context_val
(** {6 Saving proofs } *)
-type proof_info
-
-val default_info : proof_info
+type lemma_info
+val default_lemma_info : lemma_info
val save_lemma_admitted
- : ?proof:(Proof_global.proof_object * proof_info)
+ : ?proof:(Proof_global.proof_object * lemma_info)
-> lemma:t
-> unit
val save_lemma_proved
- : ?proof:(Proof_global.proof_object * proof_info)
+ : ?proof:(Proof_global.proof_object * lemma_info)
-> ?lemma:t
-> opaque:Proof_global.opacity_flag
-> idopt:Names.lident option
@@ -126,5 +137,6 @@ val save_lemma_proved
(* To be removed *)
module Internal : sig
(** Only needed due to the Proof_global compatibility layer. *)
- val get_info : t -> proof_info
+ val get_info : t -> lemma_info
+
end
diff --git a/vernac/vernacentries.mli b/vernac/vernacentries.mli
index e46212ca1c..05de191214 100644
--- a/vernac/vernacentries.mli
+++ b/vernac/vernacentries.mli
@@ -22,7 +22,7 @@ val vernac_require :
(** The main interpretation function of vernacular expressions *)
val interp :
?verbosely:bool ->
- ?proof:(Proof_global.proof_object * Lemmas.proof_info) ->
+ ?proof:(Proof_global.proof_object * Lemmas.lemma_info) ->
st:Vernacstate.t -> Vernacexpr.vernac_control -> Vernacstate.t
(** Prepare a "match" template for a given inductive type.
diff --git a/vernac/vernacstate.ml b/vernac/vernacstate.ml
index 2bc20a747d..eabbb78d47 100644
--- a/vernac/vernacstate.ml
+++ b/vernac/vernacstate.ml
@@ -131,7 +131,7 @@ module Proof_global = struct
s_lemmas := Some stack;
res
- type closed_proof = Proof_global.proof_object * Lemmas.proof_info
+ type closed_proof = Proof_global.proof_object * Lemmas.lemma_info
let return_proof ?allow_partial () = cc (return_proof ?allow_partial)
diff --git a/vernac/vernacstate.mli b/vernac/vernacstate.mli
index 7e4d5d0315..1d292077da 100644
--- a/vernac/vernacstate.mli
+++ b/vernac/vernacstate.mli
@@ -51,7 +51,7 @@ module Proof_global : sig
val return_proof : ?allow_partial:bool -> unit -> Proof_global.closed_proof_output
- type closed_proof = Proof_global.proof_object * Lemmas.proof_info
+ type closed_proof = Proof_global.proof_object * Lemmas.lemma_info
val close_future_proof :
opaque:Proof_global.opacity_flag ->
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 13:02:18 +0000