diff options
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 |