[lemmas] Reify info for implicits, univ_decls, prepare for rec_thms.

Key information about an interactive lemma proof was stored as a
closure on an ad-hoc hook, then later made available to the hook
closing actions.

Instead, we put this information in the lemma state and incorporate
these declarations into the normal save path.

We prepare to put the information about rec_thms in the state too.

11 files changed, 122 insertions, 83 deletions

diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml
index cb4eabcc85..d00f2c4803 100644
--- a/proofs/pfedit.ml
+++ b/proofs/pfedit.ml
@@ -119,7 +119,7 @@ let next = let n = ref 0 in fun () -> incr n; !n
 let build_constant_by_tactic id ctx sign ?(goal_kind = Global ImportDefaultBehavior, false, Proof Theorem) typ tac =
   let evd = Evd.from_ctx ctx in
   let goals = [ (Global.env_of_context sign , typ) ] in
-  let pf = Proof_global.start_proof evd id goal_kind goals in
+  let pf = Proof_global.start_proof evd id UState.default_univ_decl goal_kind goals in
   try
     let pf, status = by tac pf in
     let open Proof_global in
diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml
index 4490fbdd64..dfd54594eb 100644
--- a/proofs/proof_global.ml
+++ b/proofs/proof_global.ml
@@ -91,19 +91,19 @@ let set_endline_tactic tac ps =
     end of the proof to close the proof. The proof is started in the
     evar map [sigma] (which can typically contain universe
     constraints), and with universe bindings pl. *)
-let start_proof sigma name ?(pl=UState.default_univ_decl) kind goals =
+let start_proof sigma name udecl kind goals =
   { proof = Proof.start ~name ~poly:(pi2 kind) sigma goals
   ; endline_tactic = None
   ; section_vars = None
-  ; universe_decl = pl
+  ; universe_decl = udecl
   ; strength = kind
   }
 
-let start_dependent_proof name ?(pl=UState.default_univ_decl) kind goals =
+let start_dependent_proof name udecl kind goals =
   { proof = Proof.dependent_start ~name ~poly:(pi2 kind) goals
   ; endline_tactic = None
   ; section_vars = None
-  ; universe_decl = pl
+  ; universe_decl = udecl
   ; strength = kind
   }
 
diff --git a/proofs/proof_global.mli b/proofs/proof_global.mli
index 4e1aa64e7b..17f5c73560 100644
--- a/proofs/proof_global.mli
+++ b/proofs/proof_global.mli
@@ -63,7 +63,7 @@ type opacity_flag = Opaque | Transparent
 val start_proof
   :  Evd.evar_map
   -> Names.Id.t
-  -> ?pl:UState.universe_decl
+  -> UState.universe_decl
   -> Decl_kinds.goal_kind
   -> (Environ.env * EConstr.types) list
   -> t
@@ -72,7 +72,7 @@ val start_proof
     initial goals. *)
 val start_dependent_proof
   :  Names.Id.t
-  -> ?pl:UState.universe_decl
+  -> UState.universe_decl
   -> Decl_kinds.goal_kind
   -> Proofview.telescope
   -> t
diff --git a/stm/stm.ml b/stm/stm.ml
index 89d95d0cc9..2fefb7fbb3 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -1537,7 +1537,7 @@ end = struct (* {{{ *)
 
           let st = Vernacstate.freeze_interp_state ~marshallable:false in
           stm_vernac_interp stop
-            ~proof:(pobject, Lemmas.default_info) st
+            ~proof:(pobject, Lemmas.default_lemma_info) st
             { verbose = false; indentation = 0; strlen = 0;
               expr = CAst.make ?loc @@ VernacExpr ([], VernacEndProof (Proved (opaque,None))) }) in
         ignore(Future.join checked_proof);
@@ -1677,7 +1677,7 @@ end = struct (* {{{ *)
       let pterm, _info =
         PG_compat.close_proof ~opaque ~keep_body_ucst_separate:true (fun x -> x) in
 
-      let proof = pterm, Lemmas.default_info in
+      let proof = pterm, Lemmas.default_lemma_info in
 
       (* We jump at the beginning since the kernel handles side effects by also
        * looking at the ones that happen to be present in the current env *)
diff --git a/vernac/classes.ml b/vernac/classes.ml
index d6a2f2727a..b8eb7e2ab1 100644
--- a/vernac/classes.ml
+++ b/vernac/classes.ml
@@ -366,7 +366,7 @@ let declare_instance_program env sigma ~global ~poly id pri imps decl term termt
            ~univdecl:decl typ ctx ~kind:(Global ImportDefaultBehavior,poly,Instance) ~hook obls)
 
 
-let declare_instance_open sigma ?hook ~tac ~global ~poly id pri imps decl ids term termtype =
+let declare_instance_open sigma ?hook ~tac ~global ~poly id pri imps udecl ids term termtype =
   (* spiwack: it is hard to reorder the actions to do
      the pretyping after the proof has opened. As a
      consequence, we use the low-level primitives to code
@@ -374,7 +374,7 @@ let declare_instance_open sigma ?hook ~tac ~global ~poly id pri imps decl ids te
   let gls = List.rev (Evd.future_goals sigma) in
   let sigma = Evd.reset_future_goals sigma in
   let kind = Decl_kinds.(Global ImportDefaultBehavior, poly, DefinitionBody Instance) in
-  let lemma = Lemmas.start_lemma id ~pl:decl kind sigma (EConstr.of_constr termtype)
+  let lemma = Lemmas.start_lemma id ~udecl kind sigma (EConstr.of_constr termtype)
       ~hook:(DeclareDef.Hook.make
                (fun _ _ _ -> instance_hook pri global imps ?hook)) in
   (* spiwack: I don't know what to do with the status here. *)
diff --git a/vernac/comFixpoint.ml b/vernac/comFixpoint.ml
index a88413cf7f..d5fb2a140c 100644
--- a/vernac/comFixpoint.ml
+++ b/vernac/comFixpoint.ml
@@ -261,8 +261,10 @@ let declare_fixpoint_notations ntns =
 let declare_fixpoint_interactive local poly ((fixnames,fixrs,fixdefs,fixtypes),pl,ctx,fiximps) indexes ntns =
   (* Some bodies to define by proof *)
   let thms =
-    List.map3 (fun id t (ctx,imps,_) -> (id,(EConstr.of_constr t,(List.map RelDecl.get_name ctx,imps))))
-              fixnames fixtypes fiximps in
+    List.map3 (fun name t (ctx,impargs,_) ->
+        { Lemmas.Recthm.name; typ = EConstr.of_constr t
+        ; args = List.map RelDecl.get_name ctx; impargs})
+      fixnames fixtypes fiximps in
   let init_tac =
     Some (List.map (Option.cata (EConstr.of_constr %> Tactics.exact_no_check) Tacticals.New.tclIDTAC)
       fixdefs) in
@@ -299,8 +301,10 @@ let declare_cofixpoint_notations = declare_fixpoint_notations
 let declare_cofixpoint_interactive local poly ((fixnames,fixrs,fixdefs,fixtypes),pl,ctx,fiximps) ntns =
   (* Some bodies to define by proof *)
   let thms =
-    List.map3 (fun id t (ctx,imps,_) -> (id,(EConstr.of_constr t,(List.map RelDecl.get_name ctx,imps))))
-              fixnames fixtypes fiximps in
+    List.map3 (fun name t (ctx,impargs,_) ->
+        { Lemmas.Recthm.name; typ = EConstr.of_constr t
+        ; args = List.map RelDecl.get_name ctx; impargs})
+      fixnames fixtypes fiximps in
   let init_tac =
     Some (List.map (Option.cata (EConstr.of_constr %> Tactics.exact_no_check) Tacticals.New.tclIDTAC)
       fixdefs) in
diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml
index c2de83c1bb..6a06493bfa 100644
--- a/vernac/lemmas.ml
+++ b/vernac/lemmas.ml
@@ -56,15 +56,38 @@ module Proof_ending = struct
 
 end
 
-(* Proofs with a save constant function *)
-type t =
-  { proof : Proof_global.t
-  ; hook : DeclareDef.Hook.t option
+module Recthm = struct
+  type t =
+    { name : Id.t
+    ; typ : EConstr.t
+    ; args : Name.t list
+    ; impargs : Impargs.manual_implicits
+    }
+end
+
+type lemma_info =
+  { hook : DeclareDef.Hook.t option
   ; compute_guard : lemma_possible_guards
+  ; impargs : Impargs.manual_implicits
+  ; udecl : UState.universe_decl (* This is sadly not available on the save_proof path *)
   ; proof_ending : Proof_ending.t CEphemeron.key
   (* This could be improved and the CEphemeron removed *)
   }
 
+let default_lemma_info =
+  { hook = None
+  ; compute_guard = []
+  ; impargs = []
+  ; udecl = UState.default_univ_decl
+  ; proof_ending = CEphemeron.create Proof_ending.Regular
+  }
+
+(* Proofs with a save constant function *)
+type t =
+  { proof : Proof_global.t
+  ; info : lemma_info
+  }
+
 let pf_map f pf = { pf with proof = f pf.proof }
 let pf_fold f pf = f pf.proof
 
@@ -73,12 +96,11 @@ let set_endline_tactic t = pf_map (Proof_global.set_endline_tactic t)
 (* To be removed *)
 module Internal = struct
 
-(** Gets the current terminator without checking that the proof has
-    been completed. Useful for the likes of [Admitted]. *)
-let get_info ps = ps.hook, ps.compute_guard, ps.proof_ending
+  (** Gets the current terminator without checking that the proof has
+      been completed. Useful for the likes of [Admitted]. *)
+  let get_info ps = ps.info
 
 end
-(* Internal *)
 
 let by tac pf =
   let proof, res = Pfedit.by tac pf.proof in
@@ -221,8 +243,9 @@ let check_name_freshness locality {CAst.loc;v=id} : unit =
   then
     user_err ?loc  (Id.print id ++ str " already exists.")
 
-let save_remaining_recthms env sigma (locality,p,kind) norm univs body opaq i (id,(t_i,(_,imps))) =
-  let t_i = norm t_i in
+let save_remaining_recthms env sigma (locality,p,kind) norm univs body opaq i
+    { Recthm.name; typ; impargs } =
+  let t_i = norm typ in
   let k = IsAssumption Conjectural in
   match body with
   | None ->
@@ -236,13 +259,13 @@ let save_remaining_recthms env sigma (locality,p,kind) norm univs body opaq i (i
             | Monomorphic_entry univs -> univs
           in
           let c = SectionLocalAssum ((t_i, univs),p,impl) in
-	  let _ = declare_variable id (Lib.cwd(),c,k) in
-          (VarRef id,imps)
+          let _ = declare_variable name (Lib.cwd(),c,k) in
+          (VarRef name,impargs)
       | Global local ->
           let k = IsAssumption Conjectural in
           let decl = (ParameterEntry (None,(t_i,univs),None), k) in
-          let kn = declare_constant id ~local decl in
-          (ConstRef kn,imps))
+          let kn = declare_constant name ~local decl in
+          (ConstRef kn,impargs))
   | Some body ->
       let body = norm body in
       let k = Kindops.logical_kind_of_goal_kind kind in
@@ -259,14 +282,14 @@ let save_remaining_recthms env sigma (locality,p,kind) norm univs body opaq i (i
       | Discharge ->
           let const = definition_entry ~types:t_i ~opaque:opaq ~univs body_i in
 	  let c = SectionLocalDef const in
-	  let _ = declare_variable id (Lib.cwd(), c, k) in
-          (VarRef id,imps)
+          let _ = declare_variable name (Lib.cwd(), c, k) in
+          (VarRef name,impargs)
       | Global local ->
         let const =
           Declare.definition_entry ~types:t_i ~univs ~opaque:opaq body_i
 	in
-        let kn = declare_constant id ~local (DefinitionEntry const, k) in
-        (ConstRef kn,imps)
+        let kn = declare_constant name ~local (DefinitionEntry const, k) in
+        (ConstRef kn,impargs)
 
 let initialize_named_context_for_proof () =
   let sign = Global.named_context () in
@@ -312,33 +335,37 @@ module Stack = struct
 end
 
 (* Starting a goal *)
-let start_lemma id ?pl kind sigma ?(proof_ending = Proof_ending.Regular)
-    ?(sign=initialize_named_context_for_proof()) ?(compute_guard=[]) ?hook c =
+let start_lemma id ?(udecl = UState.default_univ_decl) kind sigma ?(proof_ending = Proof_ending.Regular)
+    ?(sign=initialize_named_context_for_proof()) ?(compute_guard=[]) ?hook ?(impargs=[]) c =
   let goals = [ Global.env_of_context sign , c ] in
-  let proof = Proof_global.start_proof sigma id ?pl kind goals in
-  { proof ; hook; compute_guard; proof_ending = CEphemeron.create proof_ending }
-
-let start_dependent_lemma id ?pl kind ?(proof_ending = Proof_ending.Regular)
-    ?(compute_guard=[]) ?hook telescope =
-  let proof = Proof_global.start_dependent_proof id ?pl kind telescope in
-  { proof; hook; compute_guard; proof_ending = CEphemeron.create proof_ending }
+  let proof = Proof_global.start_proof sigma id udecl kind goals in
+  let proof_ending = CEphemeron.create proof_ending in
+  let info = { hook; compute_guard; impargs; udecl; proof_ending } in
+  { proof ; info }
+
+let start_dependent_lemma id ?(udecl = UState.default_univ_decl) kind ?(proof_ending = Proof_ending.Regular) ?(compute_guard=[]) ?hook
+    ?(impargs=[]) telescope =
+  let proof = Proof_global.start_dependent_proof id udecl kind telescope in
+  let proof_ending = CEphemeron.create proof_ending in
+  let info = { hook; compute_guard; impargs; udecl; proof_ending } in
+  { proof; info }
 
 let rec_tac_initializer finite guard thms snl =
   if finite then
-    match List.map (fun (id,(t,_)) -> (id,t)) thms with
+    match List.map (fun { Recthm.name; typ } -> name,typ) thms with
     | (id,_)::l -> Tactics.mutual_cofix id l 0
     | _ -> assert false
   else
     (* nl is dummy: it will be recomputed at Qed-time *)
-    let nl = match snl with 
+    let nl = match snl with
      | None -> List.map succ (List.map List.last guard)
      | Some nl -> nl
-    in match List.map2 (fun (id,(t,_)) n -> (id,n, t)) thms nl with
+    in match List.map2 (fun { Recthm.name; typ } n -> (name, n, typ)) thms nl with
        | (id,n,_)::l -> Tactics.mutual_fix id n l 0
        | _ -> assert false
 
-let start_lemma_with_initialization ?hook kind sigma decl recguard thms snl =
-  let intro_tac (_, (_, (ids, _))) = Tactics.auto_intros_tac ids in
+let start_lemma_with_initialization ?hook kind sigma udecl recguard thms snl =
+  let intro_tac { Recthm.args; _ } = Tactics.auto_intros_tac args in
   let init_tac,guard = match recguard with
   | Some (finite,guard,init_tac) ->
     let rec_tac = rec_tac_initializer finite guard thms snl in
@@ -354,7 +381,7 @@ let start_lemma_with_initialization ?hook kind sigma decl recguard thms snl =
     Some (intro_tac (List.hd thms)), [] in
   match thms with
   | [] -> anomaly (Pp.str "No proof to start.")
-  | (id,(t,(_,imps)))::other_thms ->
+  | { Recthm.name; typ; impargs; _}::other_thms ->
       let hook ctx _ strength ref =
         let other_thms_data =
           if List.is_empty other_thms then [] else
@@ -362,20 +389,19 @@ let start_lemma_with_initialization ?hook kind sigma decl recguard thms snl =
             let body,opaq = retrieve_first_recthm ctx ref in
             let norm c = EConstr.to_constr (Evd.from_ctx ctx) c in
             let body = Option.map EConstr.of_constr body in
-            let uctx = UState.check_univ_decl ~poly:(pi2 kind) ctx decl in
+            let uctx = UState.check_univ_decl ~poly:(pi2 kind) ctx udecl in
             let env = Global.env () in
             List.map_i (save_remaining_recthms env sigma kind norm uctx body opaq) 1 other_thms in
-        let thms_data = (ref,imps)::other_thms_data in
+        let thms_data = (ref,impargs)::other_thms_data in
         List.iter (fun (ref,imps) ->
 	  maybe_declare_manual_implicits false ref imps;
           DeclareDef.Hook.call ?hook ctx [] strength ref) thms_data in
       let hook = DeclareDef.Hook.make hook in
-      let lemma = start_lemma id ~pl:decl kind sigma t ~hook ~compute_guard:guard in
-      let lemma = pf_map (Proof_global.map_proof (fun p ->
-          match init_tac with
-          | None -> p
-          | Some tac -> pi1 @@ Proof.run_tactic Global.(env ()) tac p)) lemma in
-      lemma
+    let lemma = start_lemma name ~impargs ~udecl kind sigma typ ~hook ~compute_guard:guard in
+    pf_map (Proof_global.map_proof (fun p ->
+        match init_tac with
+        | None -> p
+        | Some tac -> pi1 @@ Proof.run_tactic Global.(env ()) tac p)) lemma
 
 let start_lemma_com ~program_mode ?inference_hook ?hook kind thms =
   let env0 = Global.env () in
@@ -398,7 +424,8 @@ let start_lemma_com ~program_mode ?inference_hook ?hook kind thms =
   let evd = Evd.minimize_universes evd in
   (* XXX: This nf_evar is critical too!! We are normalizing twice if
      you look at the previous lines... *)
-  let thms = List.map (fun (n, (t, info)) -> (n, (nf_evar evd t, info))) thms in
+  let thms = List.map (fun (name, (typ, (args, impargs))) ->
+      { Recthm.name; typ = nf_evar evd typ; args; impargs} ) thms in
   let () =
     let open UState in
     if not (decl.univdecl_extensible_instance && decl.univdecl_extensible_constraints) then
@@ -446,7 +473,7 @@ let get_keep_admitted_vars =
 let save_lemma_admitted ?proof ~(lemma : t) =
     let open Proof_global in
     match proof with
-    | Some ({ id; entries; persistence = k; universes }, (hook, _, _)) ->
+    | Some ({ id; entries; persistence = k; universes }, { hook; _} ) ->
       if List.length entries <> 1 then
         user_err Pp.(str "Admitted does not support multiple statements");
       let { proof_entry_secctx; proof_entry_type } = List.hd entries in
@@ -483,18 +510,15 @@ let save_lemma_admitted ?proof ~(lemma : t) =
           | _ -> None in
       let decl = Proof_global.get_universe_decl lemma.proof in
       let ctx = UState.check_univ_decl ~poly universes decl in
-      finish_admitted name gk (sec_vars, (typ, ctx), None) universes lemma.hook
+      finish_admitted name gk (sec_vars, (typ, ctx), None) universes lemma.info.hook
 
 (************************************************************************)
 (* Saving a lemma-like constant                                         *)
 (************************************************************************)
 
-type proof_info = DeclareDef.Hook.t option * lemma_possible_guards * Proof_ending.t CEphemeron.key
-
-let default_info = None, [], CEphemeron.create Proof_ending.Regular
-
-let finish_proved opaque idopt po hook compute_guard =
+let finish_proved opaque idopt po info =
   let open Proof_global in
+  let { hook; compute_guard; udecl; impargs } = info in
   match po with
   | { id; entries=[const]; persistence=locality,poly,kind; universes } ->
     let is_opaque = match opaque with
@@ -615,17 +639,16 @@ let save_lemma_proved ?proof ?lemma ~opaque ~idopt =
     | None ->
       (* XXX: The close_proof and proof state API should be refactored
          so it is possible to insert proofs properly into the state *)
-      let { proof; hook; compute_guard; proof_ending } = Option.get lemma in
-      Proof_global.close_proof ~opaque ~keep_body_ucst_separate:false (fun x -> x) proof, (hook, compute_guard, proof_ending)
+      let { proof; info } = Option.get lemma in
+      Proof_global.close_proof ~opaque ~keep_body_ucst_separate:false (fun x -> x) proof, info
     | Some (proof, info) ->
       proof, info
   in
-  let hook, compute_guard, proof_ending = proof_info in
   let open Proof_global in
   let open Proof_ending in
-  match CEphemeron.default proof_ending Regular with
+  match CEphemeron.default proof_info.proof_ending Regular with
   | Regular ->
-    finish_proved opaque idopt proof_obj hook compute_guard
+    finish_proved opaque idopt proof_obj proof_info
   | End_obligation oinfo ->
     DeclareObl.obligation_terminator opaque proof_obj.entries proof_obj.universes oinfo
   | End_derive { f ; name } ->
diff --git a/vernac/lemmas.mli b/vernac/lemmas.mli
index 70c8b511a1..63b1dbb75b 100644
--- a/vernac/lemmas.mli
+++ b/vernac/lemmas.mli
@@ -60,25 +60,39 @@ module Proof_ending : sig
 
 end
 
+module Recthm : sig
+  type t =
+    { name : Id.t
+    (** Name of theorem *)
+    ; typ : EConstr.t
+    (** Type of theorem  *)
+    ; args : Name.t list
+    (** Names to pre-introduce  *)
+    ; impargs : Impargs.manual_implicits
+    }
+end
+
 val start_lemma
   :  Id.t
-  -> ?pl:UState.universe_decl
+  -> ?udecl:UState.universe_decl
   -> goal_kind
   -> Evd.evar_map
   -> ?proof_ending:Proof_ending.t
   -> ?sign:Environ.named_context_val
   -> ?compute_guard:lemma_possible_guards
   -> ?hook:DeclareDef.Hook.t
+  -> ?impargs:Impargs.manual_implicits
   -> EConstr.types
   -> t
 
 val start_dependent_lemma
   :  Id.t
-  -> ?pl:UState.universe_decl
+  -> ?udecl:UState.universe_decl
   -> goal_kind
   -> ?proof_ending:Proof_ending.t
   -> ?compute_guard:lemma_possible_guards
   -> ?hook:DeclareDef.Hook.t
+  -> ?impargs:Impargs.manual_implicits
   -> Proofview.telescope
   -> t
 
@@ -92,9 +106,7 @@ val start_lemma_with_initialization
   :  ?hook:DeclareDef.Hook.t
   -> goal_kind -> Evd.evar_map -> UState.universe_decl
   -> (bool * lemma_possible_guards * unit Proofview.tactic list option) option
-  -> (Id.t (* name of thm *) *
-     (EConstr.types (* type of thm *) *
-      (Name.t list (* names to pre-introduce *) * Impargs.manual_implicits))) list
+  -> Recthm.t list
   -> int list option
   -> t
 
@@ -107,17 +119,16 @@ val initialize_named_context_for_proof : unit -> Environ.named_context_val
 
 (** {6 Saving proofs } *)
 
-type proof_info
-
-val default_info : proof_info
+type lemma_info
+val default_lemma_info : lemma_info
 
 val save_lemma_admitted
-  :  ?proof:(Proof_global.proof_object * proof_info)
+  :  ?proof:(Proof_global.proof_object * lemma_info)
   -> lemma:t
   -> unit
 
 val save_lemma_proved
-  :  ?proof:(Proof_global.proof_object * proof_info)
+  :  ?proof:(Proof_global.proof_object * lemma_info)
   -> ?lemma:t
   -> opaque:Proof_global.opacity_flag
   -> idopt:Names.lident option
@@ -126,5 +137,6 @@ val save_lemma_proved
 (* To be removed *)
 module Internal : sig
   (** Only needed due to the Proof_global compatibility layer. *)
-  val get_info : t -> proof_info
+  val get_info : t -> lemma_info
+
 end
diff --git a/vernac/vernacentries.mli b/vernac/vernacentries.mli
index e46212ca1c..05de191214 100644
--- a/vernac/vernacentries.mli
+++ b/vernac/vernacentries.mli
@@ -22,7 +22,7 @@ val vernac_require :
 (** The main interpretation function of vernacular expressions *)
 val interp :
   ?verbosely:bool ->
-  ?proof:(Proof_global.proof_object * Lemmas.proof_info) ->
+  ?proof:(Proof_global.proof_object * Lemmas.lemma_info) ->
   st:Vernacstate.t -> Vernacexpr.vernac_control -> Vernacstate.t
 
 (** Prepare a "match" template for a given inductive type.
diff --git a/vernac/vernacstate.ml b/vernac/vernacstate.ml
index 2bc20a747d..eabbb78d47 100644
--- a/vernac/vernacstate.ml
+++ b/vernac/vernacstate.ml
@@ -131,7 +131,7 @@ module Proof_global = struct
       s_lemmas := Some stack;
       res
 
-  type closed_proof = Proof_global.proof_object * Lemmas.proof_info
+  type closed_proof = Proof_global.proof_object * Lemmas.lemma_info
 
 
   let return_proof ?allow_partial () = cc (return_proof ?allow_partial)
diff --git a/vernac/vernacstate.mli b/vernac/vernacstate.mli
index 7e4d5d0315..1d292077da 100644
--- a/vernac/vernacstate.mli
+++ b/vernac/vernacstate.mli
@@ -51,7 +51,7 @@ module Proof_global : sig
 
   val return_proof : ?allow_partial:bool -> unit -> Proof_global.closed_proof_output
 
-  type closed_proof = Proof_global.proof_object * Lemmas.proof_info
+  type closed_proof = Proof_global.proof_object * Lemmas.lemma_info
 
   val close_future_proof :
     opaque:Proof_global.opacity_flag ->