Merge PR #10316: [lemmas] Reify info for implicits, universe decls, and rec theorems.

Reviewed-by: SkySkimmer
Ack-by: ejgallego
Reviewed-by: gares
Reviewed-by: ppedrot

1 files changed, 14 insertions, 22 deletions

diff --git a/proofs/proof.ml b/proofs/proof.ml
index 47502fe402..9f2c90c375 100644
--- a/proofs/proof.ml
+++ b/proofs/proof.ml
@@ -118,8 +118,6 @@ type t =
   (** List of goals that have been shelved. *)
   ; given_up : Goal.goal list
   (** List of goals that have been given up *)
-  ; initial_euctx : UState.t
-  (** The initial universe context (for the statement) *)
   ; name : Names.Id.t
   (** the name of the theorem whose proof is being constructed *)
   ; poly : bool
@@ -290,14 +288,12 @@ let unfocused = is_last_focus end_of_stack_kind
 
 let start ~name ~poly sigma goals =
   let entry, proofview = Proofview.init sigma goals in
-  let pr = {
-    proofview;
-    entry;
-    focus_stack = [] ;
-    shelf = [] ;
-    given_up = [];
-    initial_euctx =
-      Evd.evar_universe_context (snd (Proofview.proofview proofview))
+  let pr =
+    { proofview
+    ; entry
+    ; focus_stack = []
+    ; shelf = []
+    ; given_up = []
     ; name
     ; poly
   } in
@@ -305,14 +301,12 @@ let start ~name ~poly sigma goals =
 
 let dependent_start ~name ~poly goals =
   let entry, proofview = Proofview.dependent_init goals in
-  let pr = {
-    proofview;
-    entry;
-    focus_stack = [] ;
-    shelf = [] ;
-    given_up = [];
-    initial_euctx =
-      Evd.evar_universe_context (snd (Proofview.proofview proofview))
+  let pr =
+    { proofview
+    ; entry
+    ; focus_stack = []
+    ; shelf = []
+    ; given_up = []
     ; name
     ; poly
   } in
@@ -488,15 +482,13 @@ type data =
   (** A representation of the shelf  *)
   ; given_up : Evar.t list
   (** A representation of the given up goals  *)
-  ; initial_euctx : UState.t
-  (** The initial universe context (for the statement) *)
   ; name : Names.Id.t
   (** The name of the theorem whose proof is being constructed *)
   ; poly : bool
   (** Locality, polymorphism, and "kind" [Coercion, Definition, etc...] *)
   }
 
-let data { proofview; focus_stack; entry; shelf; given_up; initial_euctx; name; poly } =
+let data { proofview; focus_stack; entry; shelf; given_up; name; poly } =
   let goals, sigma = Proofview.proofview proofview in
   (* spiwack: beware, the bottom of the stack is used by [Proof]
      internally, and should not be exposed. *)
@@ -507,7 +499,7 @@ let data { proofview; focus_stack; entry; shelf; given_up; initial_euctx; name;
   in
   let stack =
     map_minus_one (fun (_,_,c) -> Proofview.focus_context c) focus_stack in
-  { sigma; goals; entry; stack; shelf; given_up; initial_euctx; name; poly }
+  { sigma; goals; entry; stack; shelf; given_up; name; poly }
 
 let pr_proof p =
   let { goals=fg_goals; stack=bg_goals; shelf; given_up; _ } = data p in