diff options
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/proof_global.ml | 3 | ||||
| -rw-r--r-- | tactics/proof_global.mli | 2 |
2 files changed, 1 insertions, 4 deletions
diff --git a/tactics/proof_global.ml b/tactics/proof_global.ml index ca3a90ccbd..7fd1634dcf 100644 --- a/tactics/proof_global.ml +++ b/tactics/proof_global.ml @@ -27,7 +27,6 @@ module NamedDecl = Context.Named.Declaration type proof_object = { name : Names.Id.t ; entries : Evd.side_effects Declare.proof_entry list - ; poly : bool ; uctx: UState.t ; udecl : UState.universe_decl } @@ -240,7 +239,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; poly; uctx; udecl } + { name; entries; uctx; udecl } let return_proof ?(allow_partial=false) ps = let { proof } = ps in diff --git a/tactics/proof_global.mli b/tactics/proof_global.mli index 7b806f878d..f1281d1291 100644 --- a/tactics/proof_global.mli +++ b/tactics/proof_global.mli @@ -33,8 +33,6 @@ type proof_object = (** name of the proof *) ; entries : Evd.side_effects Declare.proof_entry list (** list of the proof terms (in a form suitable for definitions). *) - ; poly : bool - (** polymorphic status *) ; uctx: UState.t (** universe state *) ; udecl : UState.universe_decl |