diff --git a/vernac/declare.ml b/vernac/declare.ml index 50ee024a8f75..3022cb949271 100644 --- a/vernac/declare.ml +++ b/vernac/declare.ml @@ -814,6 +814,56 @@ module Internal = struct end +(* The word [proof] is to be understood as [justification] *) +(* A possible alternatve would be [evidence]?? *) +type closed_proof_output = ((Constr.t * Evd.side_effects) * Constr.t option) list * UState.t + +type proof_object = + | DefaultProof of + { proof : closed_proof_output + ; opaque : bool + ; using : Names.Id.Set.t option + ; keep_body_ucst_separate : UState.t option + } + | DeferredOpaqueProof of + { deferred_proof : closed_proof_output Future.computation + ; using : Names.Id.Set.t option + ; initial_proof_data : Proof.data + ; feedback_id : Stateid.t + ; initial_euctx : UState.t + } + +let future_map2_pair_list_distribute p l f = + List.map_i (fun i c -> f (Future.chain p (fun (a, b) -> (List.nth a i, b))) c) 0 l + +let process_proof ~info:Info.({ udecl; poly }) ?(is_telescope=false) = function + | DefaultProof { proof = (entries, uctx); opaque; using; keep_body_ucst_separate } -> + (* Force transparency for Derive-like dependent statements *) + let opaques = + let n = List.length entries in + List.init n (fun i -> + if i < n-1 && is_telescope then (* waiting for addition of cinfo-based opacity in #19029 *) false + else opaque) in + let entries = List.map2 (fun ((body, eff), typ) opaque -> + let uctx, univs, body = make_univs_immediate ~poly ?keep_body_ucst_separate ~opaque ~uctx ~udecl ~eff body typ in + definition_entry_core ?using ~univs ?types:typ body) entries opaques in + entries, uctx + | DeferredOpaqueProof { deferred_proof = bodies; using; initial_proof_data; feedback_id; initial_euctx } -> + let { Proof.poly; entry; sigma } = initial_proof_data in + let entries = + future_map2_pair_list_distribute bodies (Proofview.initial_goals entry) + (fun body_typ_uctx (_, _, initial_typ) -> + (* Testing if evar-closed? *) + let initial_typ = Evarutil.nf_evars_universes sigma (EConstr.Unsafe.to_constr initial_typ) in + (* The flags keep_body_ucst_separate, opaque, etc. should be consistent with evar-closedness? *) + let univs = UState.univ_entry ~poly:false initial_euctx in + let body = Future.chain body_typ_uctx (fun (((body, eff), _typ), uctx) -> + let uctx = make_univs_deferred_private_mono ~initial_euctx ~uctx ~udecl body (Some initial_typ) in + ((body, uctx), eff)) in + delayed_definition_entry ?using ~univs ~types:initial_typ ~feedback_id body) + in + entries, initial_euctx + let declare_definition_scheme ~internal ~univs ~role ~name ?loc c = let kind = Decls.(IsDefinition Scheme) in let entry = pure_definition_entry ~univs c in @@ -849,6 +899,27 @@ let declare_entry_core ~name ?(scope=Locality.default_scope) ?(clearbody=false) let declare_entry = declare_entry_core ~obls:[] +let warn_let_as_axiom = + CWarnings.create ~name:"let-as-axiom" ~category:CWarnings.CoreCategories.vernacular + Pp.(fun id -> strbrk "Let definition" ++ spc () ++ Names.Id.print id ++ + spc () ++ strbrk "declared as an axiom.") + +(* Declare an assumption when not in a section: Parameter/Axiom but also + Variable/Hypothesis seen as Local Parameter/Axiom *) +let declare_parameter ~name ~scope ~hook ~impargs ~uctx pe = + let local = match scope with + | Locality.Discharge -> warn_let_as_axiom name; Locality.ImportNeedQualified + | Locality.Global local -> local + in + let kind = Decls.(IsAssumption Conjectural) in + let decl = ParameterEntry pe in + let cst = declare_constant ~name ~local ~kind ~typing_flags:None decl in + let dref = Names.GlobRef.ConstRef cst in + let () = Impargs.maybe_declare_manual_implicits false dref impargs in + let () = assumption_message name in + let () = Hook.(call ?hook { S.uctx; obls = []; scope; dref}) in + cst + (* Using processing *) let interp_proof_using_gen f env evd cinfo using = let cextract v (fixnames, terms) = @@ -867,6 +938,43 @@ let gather_mutual_using_data = let typ, body = EConstr.(of_constr typ, of_constr body) in (name, [typ; body]) :: acc) [] +(* XXX: this should be unified with the code for non-interactive + mutuals previously on this file. *) + +let declare_possibly_mutual_definitions ~info ~cinfo proof_obj = + let entries, uctx = process_proof ~info proof_obj in + let { Info.hook; scope; clearbody; kind; typing_flags; user_warns; _ } = info in + let refs = List.map2 (fun CInfo.{name; impargs} -> + declare_entry ~name ~scope ~clearbody ~kind ?hook ~impargs ~typing_flags ~user_warns ~uctx) cinfo entries in + let () = + (* We override the temporary notations used while proving, now using the global names *) + let local = info.scope=Locality.Discharge in + CWarnings.with_warn ("-"^Notation.warning_overridden_name) + (List.iter (Metasyntax.add_notation_interpretation ~local (Global.env()))) info.ntns + in + refs + +let declare_possibly_mutual_parameters ~info ~cinfo ~uctx ?(mono_uctx_extra=UState.empty) ~sec_vars typs = + (* Note, if an initial uctx, minimize and restrict have not been done *) + (* if the uctx of an abandonned proof, minimize is redundant (see close_proof) *) + let { Info.scope; poly; hook; udecl } = info in + pi3 (List.fold_left2 ( + fun (i, subst, csts) { CInfo.name; impargs } typ -> + let uctx' = UState.restrict uctx (Vars.universes_of_constr typ) in + let univs = UState.check_univ_decl ~poly uctx' udecl in + let univs = if i = 0 then add_mono_uctx mono_uctx_extra univs else univs in + let typ = Vars.replace_vars subst typ in + let pe = { + parameter_entry_secctx = sec_vars; + parameter_entry_type = Evarutil.nf_evars_universes (Evd.from_ctx uctx) typ; + parameter_entry_universes = univs; + parameter_entry_inline_code = None; + } in + let cst = declare_parameter ~name ~scope ~hook ~impargs ~uctx pe in + let inst = instance_of_univs univs in + (i+1, (name, Constr.mkConstU (cst,inst))::subst, (cst, univs)::csts) + ) (0, [], []) cinfo typs) + let make_recursive_bodies env ~typing_flags ~possible_guard ~rec_declaration = let env = Environ.update_typing_flags ?typing_flags env in let indexes = Pretyping.search_guard env possible_guard rec_declaration in @@ -915,27 +1023,6 @@ let declare_mutual_definitions ~info ~cinfo ~opaque ~uctx ~bodies ~possible_guar List.iter (Metasyntax.add_notation_interpretation ~local:(scope=Locality.Discharge) (Global.env())) ntns; csts -let warn_let_as_axiom = - CWarnings.create ~name:"let-as-axiom" ~category:CWarnings.CoreCategories.vernacular - Pp.(fun id -> strbrk "Let definition" ++ spc () ++ Names.Id.print id ++ - spc () ++ strbrk "declared as an axiom.") - -(* Declare an assumption when not in a section: Parameter/Axiom but also - Variable/Hypothesis seen as Local Parameter/Axiom *) -let declare_parameter ~name ~scope ~hook ~impargs ~uctx pe = - let local = match scope with - | Locality.Discharge -> warn_let_as_axiom name; Locality.ImportNeedQualified - | Locality.Global local -> local - in - let kind = Decls.(IsAssumption Conjectural) in - let decl = ParameterEntry pe in - let cst = declare_constant ~name ~local ~kind ~typing_flags:None decl in - let dref = Names.GlobRef.ConstRef cst in - let () = Impargs.maybe_declare_manual_implicits false dref impargs in - let () = assumption_message name in - let () = Hook.(call ?hook { S.uctx; obls = []; scope; dref}) in - cst - (* Preparing proof entries *) let error_unresolved_evars env sigma t evars = let pr_unresolved_evar e = @@ -1615,10 +1702,6 @@ module Proof_ending = struct end -(* Alias *) -module Proof_ = Proof -module Proof = struct - module Proof_info = struct type t = @@ -1642,6 +1725,22 @@ module Proof_info = struct end +module Proof_object = struct + + type t = + { proof_object : proof_object + ; pinfo : Proof_info.t + } + +end + +(* Alias *) +module Proof_ = Proof +module Proof = struct + +type nonrec closed_proof_output = closed_proof_output +type proof_object = Proof_object.t + type t = { endline_tactic : Genarg.glob_generic_argument option ; using : Id.Set.t option @@ -1841,12 +1940,6 @@ let get_open_goals ps = (List.map (fun (l1,l2) -> List.length l1 + List.length l2) stack) + List.length (Evd.shelf sigma) -type proof_object = - { entries : proof_entry list - ; uctx: UState.t - ; pinfo : Proof_info.t - } - let warn_remaining_shelved_goals = CWarnings.create ~name:"remaining-shelved-goals" ~category:CWarnings.CoreCategories.tactics (fun () -> Pp.str"The proof has remaining shelved goals.") @@ -1886,6 +1979,25 @@ let () = CErrors.register_handler begin function | _ -> None end +let raise_non_ground_proof evd pid c = + let has_given_up = + let exception Found in + let rec aux c = + let () = match EConstr.kind evd c with + | Evar (e,_) -> if Evar.Set.mem e (Evd.given_up evd) then raise Found + | _ -> () + in + EConstr.iter evd aux c + in + try aux c; false with Found -> true + in + raise (OpenProof (pid, NonGroundResult has_given_up)) + +let check_incomplete_proof evd = + if Evd.has_shelved evd then warn_remaining_shelved_goals () + else if Evd.has_given_up evd then warn_given_up () + else if Evd.has_undefined evd then warn_remaining_unresolved_evars () + (* XXX: This is still separate from close_proof below due to drop_pt in the STM *) let prepare_proof ?(warn_incomplete=true) { proof; pinfo } = let Proof.{name=pid;entry;poly;sigma=evd} = Proof.data proof in @@ -1900,19 +2012,7 @@ let prepare_proof ?(warn_incomplete=true) { proof; pinfo } = let to_constr c = match EConstr.to_constr_opt evd c with | Some p -> p - | None -> - let has_given_up = - let exception Found in - let rec aux c = - let () = match EConstr.kind evd c with - | Evar (e,_) -> if Evar.Set.mem e (Evd.given_up evd) then raise Found - | _ -> () - in - EConstr.iter evd aux c - in - try aux c; false with Found -> true - in - raise (OpenProof (pid, NonGroundResult has_given_up)) + | None -> raise_non_ground_proof evd pid c in (* ppedrot: FIXME, this is surely wrong. There is no reason to duplicate side-effects... This may explain why one need to uniquize side-effects @@ -1935,14 +2035,8 @@ let prepare_proof ?(warn_incomplete=true) { proof; pinfo } = let rec_declaration = prepare_recursive_declaration pinfo.cinfo fixtypes fixrelevances fixbodies in let typing_flags = pinfo.info.typing_flags in fst (make_recursive_bodies env ~typing_flags ~possible_guard ~rec_declaration) in - let proofs = List.map (fun (body, typ) -> ((body, eff), typ)) proofs in - let () = - if warn_incomplete then begin - if Evd.has_shelved evd then warn_remaining_shelved_goals () - else if Evd.has_given_up evd then warn_given_up () - else if Evd.has_undefined evd then warn_remaining_unresolved_evars () - end - in + let proofs = List.map (fun (body, typ) -> ((body, eff), Some typ)) proofs in + let () = if warn_incomplete then check_incomplete_proof evd in proofs, Evd.ustate evd exception NotGuarded of @@ -1992,78 +2086,29 @@ let control_only_guard { proof; pinfo } = raise (NotGuarded (env, sigma, cofix_error, fix_errors, rec_declaration)) with Exit -> () -let close_proof ?warn_incomplete ~opaque ~keep_body_ucst_separate ps = - NewProfile.profile "close_proof" (fun () -> - - let { using; proof; initial_euctx; pinfo } = ps in - let { Proof_info.info = { Info.udecl } } = pinfo in - let { Proof.poly } = Proof.data proof in - let elist, uctx = prepare_proof ?warn_incomplete ps in - let opaques = - let n = List.length elist in - let is_derived = match CEphemeron.default pinfo.Proof_info.proof_ending Regular with End_derive -> true | _ -> false in - List.init n (fun i -> - if i < n-1 && is_derived then - (* Temporary code for setting opacity in Derive, waiting for addition of cinfo-based opacity in #19029 *) - false - else match opaque with - | Vernacexpr.Opaque -> true - | Vernacexpr.Transparent -> false) in - let make_entry ((body, eff), typ) opaque = - let keep_body_ucst_separate = if keep_body_ucst_separate then Some initial_euctx else None in - let _, univs, body = - make_univs_immediate ~poly ?keep_body_ucst_separate ~opaque ~uctx ~udecl ~eff body (Some typ) in - definition_entry_core ?using ~univs ~types:typ body - in - let entries = List.map2 make_entry elist opaques in - { entries; uctx; pinfo }) - () - -type closed_proof_output = (Constr.t * Evd.side_effects) list * UState.t +let return_proof p = (prepare_proof p : closed_proof_output) -let close_proof_delayed ~feedback_id ps (fpl : closed_proof_output Future.computation) = +let close_proof ?warn_incomplete ~opaque ~keep_body_ucst_separate (proof : t) : Proof_object.t = + NewProfile.profile "close_proof" (fun () -> + let opaque = match opaque with + | Vernacexpr.Opaque -> true + | Vernacexpr.Transparent -> false in + let keep_body_ucst_separate = if keep_body_ucst_separate then Some proof.initial_euctx else None in + { Proof_object.proof_object = + DefaultProof { proof = prepare_proof ?warn_incomplete proof; opaque; using = proof.using; keep_body_ucst_separate } + ; pinfo = proof.pinfo + }) () + +let close_proof_delayed ~feedback_id proof (fpl : closed_proof_output Future.computation) : Proof_object.t = NewProfile.profile "close_proof_delayed" (fun () -> - let { using; proof; initial_euctx; pinfo } = ps in - let { Proof_info.info = { Info.udecl } } = pinfo in - let { Proof.poly; entry; sigma } = Proof.data proof in - - (* We don't allow poly = true in this path *) - if poly then - CErrors.anomaly (Pp.str "Cannot delay universe-polymorphic constants."); - - (* Because of dependent subgoals at the beginning of proofs, we could - have existential variables in the initial types of goals, we need to - normalise them for the kernel. *) - let nf = Evarutil.nf_evars_universes (Evd.set_universe_context sigma initial_euctx) in - - (* We only support opaque proofs, this will be enforced by using - different entries soon *) - let make_entry i (_, _, types) = - (* Already checked the univ_decl for the type universes when starting the proof. *) - let univs = UState.univ_entry ~poly:false initial_euctx in - let typ = nf (EConstr.Unsafe.to_constr types) in - - (* NB: for Admitted proofs [fpl] is not valid (raises anomaly when forced) *) - Future.chain fpl (fun (pf, uctx) -> - let (body, eff) = List.nth pf i in - (* Deferred proof, we already checked the universe declaration with - the initial universes, ensure that the final universes respect - the declaration as well. If the declaration is non-extensible, - this will prevent the body from adding universes and constraints. *) - let uctx = make_univs_deferred_private_mono ~initial_euctx ~uctx ~udecl body (Some typ) in - ((body, uctx), eff)) - |> delayed_definition_entry ?using ~univs ~types:typ ~feedback_id - in - let entries = CList.map_i make_entry 0 (Proofview.initial_goals entry) in - { entries; uctx = initial_euctx; pinfo }) - () + { Proof_object.proof_object = + DeferredOpaqueProof { deferred_proof = fpl; using = proof.using; initial_proof_data = Proof.data proof.proof; + feedback_id; initial_euctx = proof.initial_euctx } + ; pinfo = proof.pinfo + }) () let close_future_proof = close_proof_delayed -let return_proof ps = - let p, uctx = prepare_proof ps in - List.map (fun ((body,eff),_) -> (body,eff)) p, uctx - let update_sigma_univs ugraph p = map ~f:(Proof.update_sigma_univs ugraph) p @@ -2077,11 +2122,12 @@ let build_constant_by_tactic ~name ?warn_incomplete ~sigma ~sign ~poly (typ : EC let pinfo = Proof_info.make ~cinfo ~info () in let pf = start_proof_core ~name ~pinfo sigma [Some sign, typ] in let pf, status = by tac pf in - let { entries; uctx } = close_proof ?warn_incomplete ~opaque:Vernacexpr.Transparent ~keep_body_ucst_separate:false pf in + let proof = close_proof ?warn_incomplete ~keep_body_ucst_separate:false ~opaque:Vernacexpr.Transparent pf in + let entries, uctx = process_proof ~info proof.proof_object in let { Proof.sigma } = Proof.data pf.proof in - let sigma = Evd.set_universe_context sigma uctx in match entries with | [ { proof_entry_body = Default { body; opaque = Transparent } } as entry] -> + let sigma = Evd.set_universe_context sigma uctx in { entry with proof_entry_body = body }, status, sigma | _ -> CErrors.anomaly Pp.(str "[build_constant_by_tactic] close_proof returned more than one proof term, or a non transparent one.") @@ -2152,64 +2198,6 @@ let get_current_context pf = let p = get pf in Proof.get_proof_context p -(* Support for mutually proved theorems *) - -(* XXX: this should be unified with the code for non-interactive - mutuals previously on this file. *) -module MutualEntry : sig - - val declare_possibly_mutual_parameters - : pinfo:Proof_info.t - -> uctx:UState.t - -> ?mono_uctx_extra:UState.t - -> sec_vars:Id.Set.t option - -> Constr.t list - -> (Constant.t * UState.named_universes_entry) list - - val declare_possibly_mutual_definitions - (* Common to all recthms *) - : pinfo:Proof_info.t - -> uctx:UState.t - -> proof_entry list - -> Names.GlobRef.t list - -end = struct - - let declare_possibly_mutual_definitions ~pinfo ~uctx entries = - let { Proof_info.info = { Info.hook; scope; clearbody; kind; typing_flags; user_warns; _ } } = pinfo in - let refs = List.map2 (fun CInfo.{name; impargs} -> - declare_entry ~name ~scope ~clearbody ~kind ?hook ~impargs ~typing_flags ~user_warns ~uctx) pinfo.Proof_info.cinfo entries in - let () = - (* We override the temporary notations used while proving, now using the global names *) - let local = pinfo.info.scope=Locality.Discharge in - CWarnings.with_warn ("-"^Notation.warning_overridden_name) - (List.iter (Metasyntax.add_notation_interpretation ~local (Global.env()))) pinfo.info.ntns - in - refs - - let declare_possibly_mutual_parameters ~pinfo ~uctx ?(mono_uctx_extra=UState.empty) ~sec_vars typs = - (* Note, if an initial uctx, minimize and restrict have not been done *) - (* if the uctx of an abandonned proof, minimize is redundant (see close_proof) *) - let { Info.scope; poly; hook; udecl } = pinfo.Proof_info.info in - pi3 (List.fold_left2 ( - fun (i, subst, csts) { CInfo.name; impargs } typ -> - let uctx' = UState.restrict uctx (Vars.universes_of_constr typ) in - let univs = UState.check_univ_decl ~poly uctx' udecl in - let univs = if i = 0 then add_mono_uctx mono_uctx_extra univs else univs in - let typ = Vars.replace_vars subst typ in - let pe = { - parameter_entry_secctx = sec_vars; - parameter_entry_type = Evarutil.nf_evars_universes (Evd.from_ctx uctx) typ; - parameter_entry_universes = univs; - parameter_entry_inline_code = None; - } in - let cst = declare_parameter ~name ~scope ~hook ~impargs ~uctx pe in - let inst = instance_of_univs univs in - (i+1, (name, Constr.mkConstU (cst,inst))::subst, (cst, univs)::csts) - ) (0, [], []) pinfo.Proof_info.cinfo typs) - -end - (************************************************************************) (* Admitting a lemma-like constant *) (************************************************************************) @@ -2250,14 +2238,15 @@ let check_type_evars_solved env sigma typ = let finish_admitted ~pm ~pinfo ~uctx ~sec_vars typs = (* If the constant was an obligation we need to update the program map *) + let { Proof_info.info; cinfo } = pinfo in match CEphemeron.default pinfo.Proof_info.proof_ending Proof_ending.Regular with | Proof_ending.End_obligation oinfo -> let declare_fun ~uctx ~mono_uctx_extra typ = - List.hd (MutualEntry.declare_possibly_mutual_parameters ~pinfo ~uctx ~sec_vars ~mono_uctx_extra [typ]) in + List.hd (declare_possibly_mutual_parameters ~info ~cinfo ~uctx ~sec_vars ~mono_uctx_extra [typ]) in let typ = match typs with [typ] -> typ | _ -> assert false in Obls_.obligation_admitted_terminator ~pm typ oinfo declare_fun sec_vars uctx | _ -> - let (_ : 'a list) = MutualEntry.declare_possibly_mutual_parameters ~pinfo ~uctx ~sec_vars typs in + let (_ : 'a list) = declare_possibly_mutual_parameters ~info ~cinfo ~uctx ~sec_vars typs in pm let save_admitted ~pm ~proof = @@ -2276,7 +2265,7 @@ let save_admitted ~pm ~proof = (* Saving a lemma-like constant *) (************************************************************************) -let finish_derived {entries; pinfo; uctx} = +let finish_derived pinfo uctx entries = let n = List.length entries in let { Proof_info.info = { Info.hook; scope; clearbody; kind; typing_flags; user_warns; poly; udecl; _ } } = pinfo in let _, _, refs, _ = @@ -2298,7 +2287,7 @@ let finish_derived {entries; pinfo; uctx} = (0, [], [], Univ.Level.Set.empty) pinfo.Proof_info.cinfo entries in refs -let finish_proved_equations ~pm ~kind ~hook i proof_obj types sigma0 = +let finish_proved_equations ~pm ~kind ~hook i entries types sigma0 = let obls = ref 1 in let sigma, recobls = @@ -2315,31 +2304,34 @@ let finish_proved_equations ~pm ~kind ~hook i proof_obj types sigma0 = let sigma, app = Evd.fresh_global (Global.env ()) sigma (GlobRef.ConstRef cst) in let sigma = Evd.define ev (EConstr.applist (app, args)) sigma in sigma, cst) sigma0 - types proof_obj.entries + types entries in let pm = hook ~pm recobls sigma in pm, List.map (fun cst -> GlobRef.ConstRef cst) recobls -let check_single_entry { entries; uctx } label = +let check_single_entry entries label = match entries with - | [entry] -> entry, uctx + | [entry] -> entry | _ -> CErrors.anomaly ~label Pp.(str "close_proof returned more than one proof term") let finish_proof ~pm proof_obj proof_info = let open Proof_ending in + let { Proof_info.info; cinfo; possible_guard } = proof_info in match CEphemeron.default proof_info.Proof_info.proof_ending Regular with | Regular -> - let {entries; uctx} = proof_obj in - pm, MutualEntry.declare_possibly_mutual_definitions ~uctx ~pinfo:proof_info entries + pm, declare_possibly_mutual_definitions ~info ~cinfo proof_obj | End_obligation oinfo -> - let entry, uctx = check_single_entry proof_obj "Obligation.save" in + let entries, uctx = process_proof ~info proof_obj in + let entry = check_single_entry entries "Obligation.save" in Obls_.obligation_terminator ~pm ~entry ~uctx ~oinfo | End_derive -> - pm, finish_derived proof_obj + let entries, uctx = process_proof ~info ~is_telescope:true proof_obj in + pm, finish_derived proof_info uctx entries | End_equations { hook; i; types; sigma } -> - let kind = proof_info.Proof_info.info.Info.kind in - finish_proved_equations ~pm ~kind ~hook i proof_obj types sigma + let kind = info.Info.kind in + let entries, uctx = process_proof ~info proof_obj in + finish_proved_equations ~pm ~kind ~hook i entries 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") @@ -2361,7 +2353,7 @@ let save ~pm ~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.pinfo in - finish_proof ~pm proof_obj proof_info + finish_proof ~pm proof_obj.proof_object proof_info let save_regular ~(proof : t) ~opaque ~idopt = let open Proof_ending in @@ -2375,7 +2367,8 @@ let save_regular ~(proof : t) ~opaque ~idopt = (* Special case to close a lemma without forcing a proof *) (***********************************************************************) let save_lemma_admitted_delayed ~pm ~proof = - let { entries; uctx; pinfo } = proof in + let { Proof_object.proof_object; pinfo } = proof in + let entries, uctx = process_proof ~info:pinfo.info proof_object in let typs = List.map (function { proof_entry_type } -> Option.get proof_entry_type) entries in (* Note: an alternative would be to compute sec_vars of the partial proof as a Future computation, as in compute_proof_using_for_admitted *) @@ -2383,12 +2376,12 @@ let save_lemma_admitted_delayed ~pm ~proof = (* If the proof is partial, do we want to take the (restriction on visible uvars of) uctx so far or (as done below) the initial ones that refers to only the types *) - finish_admitted ~pm ~uctx ~pinfo ~sec_vars typs + finish_admitted ~pm ~uctx ~pinfo:proof.pinfo ~sec_vars typs let save_lemma_proved_delayed ~pm ~proof ~idopt = (* vio2vo used to call this with invalid [pinfo], now it should work fine. *) - let pinfo = process_idopt_for_save ~idopt proof.pinfo in - let pm, _ = finish_proof ~pm proof pinfo in + let pinfo = process_idopt_for_save ~idopt proof.Proof_object.pinfo in + let pm, _ = finish_proof ~pm proof.proof_object pinfo in pm end (* Proof module *)