diff options
| author | Gaëtan Gilbert | 2020-03-31 11:05:21 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert | 2020-03-31 11:05:21 +0200 |
| commit | 29bcd98d55ccb9a90dff7fc8f254578c4d870a09 (patch) | |
| tree | c87bee672d196212e4f0033804e57c00deadeef8 /tactics | |
| parent | c31a634b1f57028f3491b61137e53978d2653bbe (diff) | |
| parent | 1320d5004b58f33c2274bfdc0629d7f513cd49c4 (diff) | |
Merge PR #11818: [proof] Further consolidation of the regular declaration path
Ack-by: Matafou
Reviewed-by: SkySkimmer
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 |