diff options
| author | Emilio Jesus Gallego Arias | 2019-10-24 20:31:09 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2019-10-28 17:02:32 +0100 |
| commit | b27f54b04f50d3fad0eedd9c46366fd2bb612987 (patch) | |
| tree | 3e501d91de1ca811786e835a598b1d4220fb65e7 /tactics | |
| parent | 42eac2b1cee72acce4ebf0ce3e74dd60763b223b (diff) | |
[declare] Provide helper for private constant inlining.
We factor some duplicate code, this is a step towards making the
`proof_entry` type abstract.
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/declare.ml | 6 | ||||
| -rw-r--r-- | tactics/declare.mli | 9 | ||||
| -rw-r--r-- | tactics/pfedit.ml | 11 |
3 files changed, 21 insertions, 5 deletions
diff --git a/tactics/declare.ml b/tactics/declare.ml index 57eeddb847..dcbd28f829 100644 --- a/tactics/declare.ml +++ b/tactics/declare.ml @@ -326,6 +326,12 @@ let declare_private_constant ?role ?(local = ImportDefaultBehavior) ~name ~kind let eff = { Evd.seff_private = eff; Evd.seff_roles; } in kn, eff +let inline_private_constants ~univs env ce = + let body, eff = Future.force ce.proof_entry_body in + let cb, ctx = Safe_typing.inline_private_constants env (body, eff.Evd.seff_private) in + let univs = UState.merge ~sideff:true Evd.univ_rigid univs ctx in + cb, univs + (** Declaration of section variables and local definitions *) type variable_declaration = | SectionLocalDef of Evd.side_effects proof_entry diff --git a/tactics/declare.mli b/tactics/declare.mli index 1a037ef937..439f0018aa 100644 --- a/tactics/declare.mli +++ b/tactics/declare.mli @@ -83,6 +83,15 @@ val declare_private_constant -> unit proof_entry -> Constant.t * Evd.side_effects +(** [inline_private_constants ~sideff ~univs env ce] will inline the + constants in [ce]'s body and return the body plus the updated + [UState.t]. *) +val inline_private_constants + : univs:UState.t + -> Environ.env + -> Evd.side_effects proof_entry + -> Constr.t * UState.t + (** Since transparent constants' side effects are globally declared, we * need that *) val set_declare_scheme : diff --git a/tactics/pfedit.ml b/tactics/pfedit.ml index 413c6540a3..c470ea04c7 100644 --- a/tactics/pfedit.ml +++ b/tactics/pfedit.ml @@ -135,12 +135,13 @@ let build_by_tactic ?(side_eff=true) env sigma ~poly typ tac = let name = Id.of_string ("temporary_proof"^string_of_int (next())) in let sign = val_of_named_context (named_context env) in let ce, status, univs = build_constant_by_tactic ~name sigma sign ~poly typ tac in - let body, eff = Future.force ce.Declare.proof_entry_body in - let (cb, ctx) = - if side_eff then Safe_typing.inline_private_constants env (body, eff.Evd.seff_private) - else body + let cb, univs = + if side_eff then Declare.inline_private_constants ~univs env ce + else + (* GG: side effects won't get reset: no need to treat their universes specially *) + let (cb, ctx), _eff = Future.force ce.Declare.proof_entry_body in + cb, UState.merge ~sideff:false Evd.univ_rigid univs ctx in - let univs = UState.merge ~sideff:side_eff Evd.univ_rigid univs ctx in cb, status, univs let refine_by_tactic ~name ~poly env sigma ty tac = |