diff options
| author | Emilio Jesus Gallego Arias | 2020-03-09 06:32:00 -0400 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2020-03-30 19:05:36 -0400 |
| commit | 5f937b2f8532b2ccf36c62557934cc2c9150005b (patch) | |
| tree | 3c08d6e963654ad191b4b313f989976ed84a5efb /tactics | |
| parent | 5749a2360f9d0d7c8901a1264863339442964ca7 (diff) | |
[proof] Miscellaneous cleanup on proof info handling
After the refactorings proof information is organized in a slightly
different way thus the lower layers don't need to pass info back
anymore.
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/proof_global.ml | 4 | ||||
| -rw-r--r-- | tactics/proof_global.mli | 2 |
2 files changed, 2 insertions, 4 deletions
diff --git a/tactics/proof_global.ml b/tactics/proof_global.ml index 623e6b8a42..620afbaf23 100644 --- a/tactics/proof_global.ml +++ b/tactics/proof_global.ml @@ -18,9 +18,9 @@ module NamedDecl = Context.Named.Declaration type proof_object = { name : Names.Id.t + (* [name] only used in the STM *) ; entries : Evd.side_effects Declare.proof_entry list ; uctx: UState.t - ; udecl : UState.universe_decl } type opacity_flag = Opaque | Transparent @@ -231,7 +231,7 @@ let close_proof ~opaque ~keep_body_ucst_separate ?feedback_id ~now Declare.delayed_definition_entry ~opaque ?feedback_id ?section_vars ~univs ~types:typ body in let entries = Future.map2 entry_fn fpl (Proofview.initial_goals entry) in - { name; entries; uctx; udecl } + { name; entries; uctx } let return_proof ?(allow_partial=false) ps = let { proof } = ps in diff --git a/tactics/proof_global.mli b/tactics/proof_global.mli index e1c75c0649..d820fc8b40 100644 --- a/tactics/proof_global.mli +++ b/tactics/proof_global.mli @@ -33,8 +33,6 @@ type proof_object = (** list of the proof terms (in a form suitable for definitions). *) ; uctx: UState.t (** universe state *) - ; udecl : UState.universe_decl - (** universe declaration *) } type opacity_flag = Opaque | Transparent |