From 5f937b2f8532b2ccf36c62557934cc2c9150005b Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Mon, 9 Mar 2020 06:32:00 -0400
Subject: [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.
---
 tactics/proof_global.ml  | 4 ++--
 tactics/proof_global.mli | 2 --
 2 files changed, 2 insertions(+), 4 deletions(-)

(limited to 'tactics')

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
-- 
cgit v1.2.3