diff options
| author | Emilio Jesus Gallego Arias | 2019-06-09 18:51:39 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2019-06-24 20:53:41 +0200 |
| commit | 599f61a45769d5938758e0fcbd479b9c8f493a58 (patch) | |
| tree | 07d471e5c84cd67898d04c2f760af77bad785985 /proofs | |
| parent | 4fe8612fbfd1581b23bb4c813c900ab687797814 (diff) | |
[lemmas] Reify info for implicits, univ_decls, prepare for rec_thms.
Key information about an interactive lemma proof was stored as a
closure on an ad-hoc hook, then later made available to the hook
closing actions.
Instead, we put this information in the lemma state and incorporate
these declarations into the normal save path.
We prepare to put the information about rec_thms in the state too.
Diffstat (limited to 'proofs')
| -rw-r--r-- | proofs/pfedit.ml | 2 | ||||
| -rw-r--r-- | proofs/proof_global.ml | 8 | ||||
| -rw-r--r-- | proofs/proof_global.mli | 4 |
3 files changed, 7 insertions, 7 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 |