diff options
| -rw-r--r-- | vernac/declare.ml | 20 | ||||
| -rw-r--r-- | vernac/declare.mli | 2 | ||||
| -rw-r--r-- | vernac/lemmas.ml | 16 |
3 files changed, 19 insertions, 19 deletions
diff --git a/vernac/declare.ml b/vernac/declare.ml index 59922c662a..e039cbc771 100644 --- a/vernac/declare.ml +++ b/vernac/declare.ml @@ -60,12 +60,25 @@ let compact_the_proof pf = map_proof Proof.compact pf let set_endline_tactic tac ps = { ps with endline_tactic = Some tac } +let initialize_named_context_for_proof () = + let sign = Global.named_context () in + List.fold_right + (fun d signv -> + let id = NamedDecl.get_id d in + 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 ~name ~udecl ~poly sigma goals = +let start_proof_core ~name ~udecl ~poly ?(sign=initialize_named_context_for_proof ()) sigma typ = + (* 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 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 { proof @@ -75,6 +88,8 @@ let start_proof ~name ~udecl ~poly sigma goals = ; initial_euctx } +let start_proof = start_proof_core ?sign:None + let start_dependent_proof ~name ~udecl ~poly goals = let proof = Proof.dependent_start ~name ~poly goals in let initial_euctx = Evd.evar_universe_context Proof.((data proof).sigma) in @@ -759,8 +774,7 @@ let by tac = map_fold_proof (Proof.solve (Goal_select.SelectNth 1) None tac) let build_constant_by_tactic ~name ?(opaque=Transparent) ~uctx ~sign ~poly typ tac = let evd = Evd.from_ctx uctx in - let goals = [ (Global.env_of_context sign , typ) ] in - let pf = start_proof ~name ~poly ~udecl:UState.default_univ_decl evd goals in + let pf = start_proof_core ~name ~poly ~sign ~udecl:UState.default_univ_decl evd typ in let pf, status = by tac pf in let { entries; uctx } = close_proof ~opaque ~keep_body_ucst_separate:false pf in match entries with diff --git a/vernac/declare.mli b/vernac/declare.mli index 979bdd4334..4023b082b3 100644 --- a/vernac/declare.mli +++ b/vernac/declare.mli @@ -84,7 +84,7 @@ val start_proof -> udecl:UState.universe_decl -> poly:bool -> Evd.evar_map - -> (Environ.env * EConstr.types) list + -> EConstr.t -> Proof.t (** Like [start_proof] except that there may be dependencies between diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml index 10d63ff2ff..c0e30e926c 100644 --- a/vernac/lemmas.ml +++ b/vernac/lemmas.ml @@ -13,8 +13,6 @@ open Util -module NamedDecl = Context.Named.Declaration - (* Support for terminators and proofs with an associated constant [that can be saved] *) @@ -51,23 +49,11 @@ let by tac pf = (* Creating a lemma-like constant *) (************************************************************************) -let initialize_named_context_for_proof () = - let sign = Global.named_context () in - List.fold_right - (fun d signv -> - let id = NamedDecl.get_id d in - 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 - (* Starting a goal *) let start_lemma ~name ~poly ?(udecl=UState.default_univ_decl) ?(info=Info.make ()) ?(impargs=[]) sigma c = - (* We remove the bodies of variables in the named context marked - "opaque", this is a hack tho, see #10446 *) - let sign = initialize_named_context_for_proof () in - let goals = [ Global.env_of_context sign , c ] in - let proof = Declare.start_proof sigma ~name ~udecl ~poly goals in + let proof = Declare.start_proof sigma ~name ~udecl ~poly c in let info = Declare.Info.add_first_thm ~info ~name ~typ:c ~impargs in { proof; info } |