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/declare.ml | |
| 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/declare.ml')
| -rw-r--r-- | tactics/declare.ml | 6 |
1 files changed, 6 insertions, 0 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 |