diff options
| author | Emilio Jesus Gallego Arias | 2020-03-07 00:32:08 -0500 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2020-03-19 17:18:55 -0400 |
| commit | a7ee674ba3330c9a0e460de6e39cffdb0f6e8805 (patch) | |
| tree | 80f4b731dbcba6712338c68c6fc01c7832f37082 /tactics | |
| parent | 1a18c20ba374a74bc7dda0c4719258b93afb149e (diff) | |
[proof] Remove duplicated poly field in Proof_global.t
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 |