[lemmas] Turn Lemmas.info into a proper type with constructor.

Lemmas.info was a bit out of hand, as well as the parameters to the
`start_*` family. Most of the info is not needed and should hopefully
remain constrained to special cases, most callers only set the hook,
and obligations should be better served by a `start_obligation`
function soon.

16 files changed, 148 insertions, 111 deletions

diff --git a/plugins/derive/derive.ml b/plugins/derive/derive.ml
index 72ca5dc8c4..22e20e2c52 100644
--- a/plugins/derive/derive.ml
+++ b/plugins/derive/derive.ml
@@ -39,8 +39,8 @@ let start_deriving f suchthat name : Lemmas.t =
                 TNil sigma))))))
   in
 
-  let proof_ending = Lemmas.Proof_ending.(End_derive {f; name}) in
-  let lemma = Lemmas.start_dependent_lemma name kind goals ~proof_ending in
+  let info = Lemmas.Info.make ~proof_ending:(Lemmas.Proof_ending.(End_derive {f; name})) () in
+  let lemma = Lemmas.start_dependent_lemma ~name ~kind ~info goals in
   Lemmas.pf_map (Proof_global.map_proof begin fun p ->
     Util.pi1 @@ Proof.run_tactic env Proofview.(tclFOCUS 1 2 shelve) p
   end) lemma
diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml
index ce3b5a82d6..9c593a55d8 100644
--- a/plugins/funind/functional_principles_proofs.ml
+++ b/plugins/funind/functional_principles_proofs.ml
@@ -994,10 +994,11 @@ let generate_equation_lemma evd fnames f fun_num nb_params nb_args rec_args_num
     (*i The next call to mk_equation_id is valid since we are constructing the lemma
       Ensures by: obvious
       i*)
-    (mk_equation_id f_id)
-    Decl_kinds.(Global ImportDefaultBehavior, false, Proof Theorem)
-    evd
-  lemma_type
+      ~name:(mk_equation_id f_id)
+      ~kind:Decl_kinds.(Global ImportDefaultBehavior, false, Proof Theorem)
+
+      evd
+      lemma_type
   in
   let lemma,_ = Lemmas.by (Proofview.V82.tactic prove_replacement) lemma in
   let () = Lemmas.save_lemma_proved ?proof:None ~lemma ~opaque:Proof_global.Transparent ~idopt:None in
diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml
index d49d657d38..1154198d43 100644
--- a/plugins/funind/functional_principles_types.ml
+++ b/plugins/funind/functional_principles_types.ml
@@ -308,9 +308,8 @@ let build_functional_principle (evd:Evd.evar_map ref) interactive_proof old_prin
   evd := sigma;
   let hook = DeclareDef.Hook.make (hook new_principle_type) in
   let lemma =
-    Lemmas.start_lemma
-      new_princ_name
-      Decl_kinds.(Global ImportDefaultBehavior,false,Proof Theorem)
+    Lemmas.start_lemma ~name:new_princ_name
+      ~kind:Decl_kinds.(Global ImportDefaultBehavior,false,Proof Theorem)
       !evd
       (EConstr.of_constr new_principle_type)
   in
diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml
index 2020881c7c..48b5e56635 100644
--- a/plugins/funind/invfun.ml
+++ b/plugins/funind/invfun.ml
@@ -804,10 +804,10 @@ let derive_correctness make_scheme (funs: pconstant list) (graphs:inductive list
          let lem_id = mk_correct_id f_id in
          let (typ,_) = lemmas_types_infos.(i) in
          let lemma = Lemmas.start_lemma
-           lem_id
-           Decl_kinds.(Global ImportDefaultBehavior,false,Proof Theorem)
-           !evd
-           typ in
+             ~name:lem_id
+             ~kind:Decl_kinds.(Global ImportDefaultBehavior,false,Proof Theorem)
+             !evd
+             typ in
          let lemma = fst @@ Lemmas.by
                    (Proofview.V82.tactic (observe_tac ("prove correctness ("^(Id.to_string f_id)^")")
                                                       (proving_tac i))) lemma in
@@ -865,8 +865,8 @@ let derive_correctness make_scheme (funs: pconstant list) (graphs:inductive list
              Ensures by: obvious
            i*)
          let lem_id = mk_complete_id f_id in
-         let lemma = Lemmas.start_lemma lem_id
-           Decl_kinds.(Global ImportDefaultBehavior,false,Proof Theorem) sigma
+         let lemma = Lemmas.start_lemma ~name:lem_id
+           ~kind:Decl_kinds.(Global ImportDefaultBehavior,false,Proof Theorem) sigma
          (fst lemmas_types_infos.(i)) in
          let lemma = fst (Lemmas.by
            (Proofview.V82.tactic (observe_tac ("prove completeness ("^(Id.to_string f_id)^")")
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index 2647e7449b..c97b39ff79 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -1367,10 +1367,11 @@ let open_new_goal ~lemma build_proof sigma using_lemmas ref_ goal_name (gls_type
     in
     Lemmas.save_lemma_proved ?proof:None ~lemma ~opaque:opacity ~idopt:None
   in
+  let info = Lemmas.Info.make ~hook:(DeclareDef.Hook.make hook) () in
   let lemma = Lemmas.start_lemma
-    na
-    Decl_kinds.(Global ImportDefaultBehavior, false (* FIXME *), Proof Lemma)
-    sigma gls_type ~hook:(DeclareDef.Hook.make hook) in
+      ~name:na
+      ~kind:Decl_kinds.(Global ImportDefaultBehavior, false (* FIXME *), Proof Lemma) ~info
+      sigma gls_type in
   let lemma = if Indfun_common.is_strict_tcc  ()
   then
     fst @@ Lemmas.by (Proofview.V82.tactic (tclIDTAC)) lemma
@@ -1408,9 +1409,13 @@ let com_terminate
     nb_args ctx
     hook =
   let start_proof env ctx (tac_start:tactic) (tac_end:tactic) =
-    let lemma = Lemmas.start_lemma thm_name
-      (Global ImportDefaultBehavior, false (* FIXME *), Proof Lemma) ~sign:(Environ.named_context_val env)
-      ctx (EConstr.of_constr (compute_terminate_type nb_args fonctional_ref)) ~hook in
+    let info = Lemmas.Info.make ~hook () in
+    let lemma = Lemmas.start_lemma ~name:thm_name
+        ~kind:(Global ImportDefaultBehavior, false (* FIXME *), Proof Lemma)
+        ~sign:(Environ.named_context_val env)
+        ~info
+        ctx
+        (EConstr.of_constr (compute_terminate_type nb_args fonctional_ref)) in
     let lemma = fst @@ Lemmas.by (Proofview.V82.tactic (observe_tac (fun _ _ -> str "starting_tac") tac_start)) lemma in
     fst @@ Lemmas.by (Proofview.V82.tactic (observe_tac (fun _ _ -> str "whole_start") (whole_start tac_end nb_args is_mes fonctional_ref
                                    input_type relation rec_arg_num ))) lemma
@@ -1455,7 +1460,7 @@ let com_eqn sign uctx nb_arg eq_name functional_ref f_ref terminate_ref equation
     let evd = Evd.from_ctx uctx in
     let f_constr = constr_of_monomorphic_global f_ref in
     let equation_lemma_type = subst1 f_constr equation_lemma_type in
-    let lemma = Lemmas.start_lemma eq_name (Global ImportDefaultBehavior, false, Proof Lemma) ~sign evd
+    let lemma = Lemmas.start_lemma ~name:eq_name ~kind:(Global ImportDefaultBehavior, false, Proof Lemma) ~sign evd
        (EConstr.of_constr equation_lemma_type) in
     let lemma = fst @@ Lemmas.by
        (Proofview.V82.tactic (start_equation f_ref terminate_ref
diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml
index f977ba34d2..49265802ae 100644
--- a/plugins/ltac/rewrite.ml
+++ b/plugins/ltac/rewrite.ml
@@ -2007,9 +2007,10 @@ let add_morphism_interactive atts m n : Lemmas.t =
     | _ -> assert false
   in
   let hook = DeclareDef.Hook.make hook in
+  let info = Lemmas.Info.make ~hook () in
   Flags.silently
     (fun () ->
-       let lemma = Lemmas.start_lemma ~hook instance_id kind (Evd.from_ctx uctx) (EConstr.of_constr instance) in
+       let lemma = Lemmas.start_lemma ~name:instance_id ~kind ~info (Evd.from_ctx uctx) (EConstr.of_constr instance) in
        fst (Lemmas.by (Tacinterp.interp tac) lemma)) ()
 
 let add_morphism atts binders m s n =
diff --git a/stm/stm.ml b/stm/stm.ml
index 2fefb7fbb3..b73d3dcdeb 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_lemma_info) st
+            ~proof:(pobject, Lemmas.Info.make ()) 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_lemma_info in
+      let proof = pterm, Lemmas.Info.make () 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 b8eb7e2ab1..51fddf1563 100644
--- a/vernac/classes.ml
+++ b/vernac/classes.ml
@@ -374,9 +374,9 @@ let declare_instance_open sigma ?hook ~tac ~global ~poly id pri imps udecl ids t
   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 ~udecl kind sigma (EConstr.of_constr termtype)
-      ~hook:(DeclareDef.Hook.make
-               (fun _ _ _ -> instance_hook pri global imps ?hook)) in
+  let hook = DeclareDef.Hook.make (fun _ _ _ -> instance_hook pri global imps ?hook) in
+  let info = Lemmas.Info.make ~udecl ~hook () in
+  let lemma = Lemmas.start_lemma ~name:id ~kind ~info sigma (EConstr.of_constr termtype) in
   (* spiwack: I don't know what to do with the status here. *)
   let lemma =
     if not (Option.is_empty term) then
diff --git a/vernac/comFixpoint.ml b/vernac/comFixpoint.ml
index 62f16961a3..31c2053148 100644
--- a/vernac/comFixpoint.ml
+++ b/vernac/comFixpoint.ml
@@ -255,7 +255,7 @@ let interp_fixpoint ~cofix l ntns =
   let uctx,fix = ground_fixpoint env evd fix in
   (fix,pl,uctx,info)
 
-let declare_fixpoint_interactive_generic ?indexes local poly ((fixnames,_fixrs,fixdefs,fixtypes),pl,ctx,fiximps) ntns =
+let declare_fixpoint_interactive_generic ?indexes local poly ((fixnames,_fixrs,fixdefs,fixtypes),udecl,ctx,fiximps) ntns =
   let fix_kind, cofix, indexes = match indexes with
     | Some indexes -> Fixpoint, false, indexes
     | None -> CoFixpoint, true, []
@@ -269,8 +269,8 @@ let declare_fixpoint_interactive_generic ?indexes local poly ((fixnames,_fixrs,f
     Some (List.map (Option.cata (EConstr.of_constr %> Tactics.exact_no_check) Tacticals.New.tclIDTAC) fixdefs) in
   let evd = Evd.from_ctx ctx in
   let lemma =
-    Lemmas.start_lemma_with_initialization (local,poly,DefinitionBody fix_kind)
-      evd pl (Some(cofix,indexes,init_tac)) thms None in
+    Lemmas.start_lemma_with_initialization ~kind:(local,poly,DefinitionBody fix_kind) ~udecl
+      evd (Some(cofix,indexes,init_tac)) thms None in
   (* Declare notations *)
   List.iter (Metasyntax.add_notation_interpretation (Global.env())) ntns;
   lemma
diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml
index 671febb528..e4415de8f2 100644
--- a/vernac/lemmas.ml
+++ b/vernac/lemmas.ml
@@ -65,29 +65,34 @@ module Recthm = struct
     }
 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 *)
-  ; other_thms : Recthm.t list
-  }
+module Info = struct
 
-let default_lemma_info =
-  { hook = None
-  ; compute_guard = []
-  ; impargs = []
-  ; udecl = UState.default_univ_decl
-  ; proof_ending = CEphemeron.create Proof_ending.Regular
-  ; other_thms = []
-  }
+  type t =
+    { 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 so we
+       duplicate it here *)
+    ; proof_ending : Proof_ending.t CEphemeron.key
+    (* This could be improved and the CEphemeron removed *)
+    ; other_thms : Recthm.t list
+    }
+
+  let make ?hook ?(udecl=UState.default_univ_decl) ?(proof_ending=Proof_ending.Regular) () =
+    { hook
+    ; compute_guard = []
+    ; impargs = []
+    ; udecl
+    ; proof_ending = CEphemeron.create proof_ending
+    ; other_thms = []
+    }
+end
 
 (* Proofs with a save constant function *)
 type t =
   { proof : Proof_global.t
-  ; info : lemma_info
+  ; info : Info.t
   }
 
 let pf_map f pf = { pf with proof = f pf.proof }
@@ -337,19 +342,14 @@ module Stack = struct
 end
 
 (* Starting a goal *)
-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=[]) ?(other_thms=[]) c =
+let start_lemma ~name ~kind ?(sign=initialize_named_context_for_proof())
+    ?(info=Info.make ()) sigma  c =
   let goals = [ Global.env_of_context sign , c ] in
-  let proof_ending = CEphemeron.create proof_ending in
-  let proof = Proof_global.start_proof sigma id udecl kind goals in
-  let info = { hook; compute_guard; impargs; udecl; proof_ending; other_thms } in
+  let proof = Proof_global.start_proof sigma name info.Info.udecl kind goals in
   { proof ; info }
 
-let start_dependent_lemma id ?(udecl = UState.default_univ_decl) kind ?(proof_ending = Proof_ending.Regular) ?(compute_guard=[]) ?hook
-    ?(impargs=[]) ?(other_thms=[]) 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; other_thms } in
+let start_dependent_lemma ~name ~kind ?(info=Info.make ()) telescope =
+  let proof = Proof_global.start_dependent_proof name info.Info.udecl kind telescope in
   { proof; info }
 
 let rec_tac_initializer finite guard thms snl =
@@ -366,9 +366,9 @@ let rec_tac_initializer finite guard thms snl =
        | (id,n,_)::l -> Tactics.mutual_fix id n l 0
        | _ -> assert false
 
-let start_lemma_with_initialization ?hook kind sigma udecl recguard thms snl =
+let start_lemma_with_initialization ?hook ~kind ~udecl sigma recguard thms snl =
   let intro_tac { Recthm.args; _ } = Tactics.auto_intros_tac args in
-  let init_tac,guard = match recguard with
+  let init_tac, compute_guard = match recguard with
   | Some (finite,guard,init_tac) ->
     let rec_tac = rec_tac_initializer finite guard thms snl in
     Some (match init_tac with
@@ -384,16 +384,24 @@ let start_lemma_with_initialization ?hook kind sigma udecl recguard thms snl =
   match thms with
   | [] -> anomaly (Pp.str "No proof to start.")
   | { Recthm.name; typ; impargs; _}::other_thms ->
-    let lemma = start_lemma name ~impargs ~udecl kind sigma typ ?hook ~other_thms ~compute_guard:guard in
+    let info =
+      Info.{ hook
+           ; udecl
+           ; impargs
+           ; compute_guard
+           ; other_thms
+           ; proof_ending = CEphemeron.create Proof_ending.Regular
+           } in
+    let lemma = start_lemma ~name ~kind ~info sigma typ 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 start_lemma_com ~program_mode ~kind ?inference_hook ?hook thms =
   let env0 = Global.env () in
   let decl = fst (List.hd thms) in
-  let evd, decl = Constrexpr_ops.interp_univ_decl_opt env0 (snd decl) in
+  let evd, udecl = Constrexpr_ops.interp_univ_decl_opt env0 (snd decl) in
   let evd, thms = List.fold_left_map (fun evd ((id, _), (bl, t)) ->
     let evd, (impls, ((env, ctx), imps)) = interp_context_evars ~program_mode env0 evd bl in
     let evd, (t', imps') = interp_type_evars_impls ~program_mode ~impls env evd t in
@@ -415,15 +423,15 @@ let start_lemma_com ~program_mode ?inference_hook ?hook kind thms =
       { 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
-       ignore (Evd.check_univ_decl ~poly:(pi2 kind) evd decl)
+    if not (udecl.univdecl_extensible_instance && udecl.univdecl_extensible_constraints) then
+       ignore (Evd.check_univ_decl ~poly:(pi2 kind) evd udecl)
   in
   let evd =
     if pi2 kind then evd
     else (* We fix the variables to ensure they won't be lowered to Set *)
       Evd.fix_undefined_variables evd
   in
-  start_lemma_with_initialization ?hook kind evd decl recguard thms snl
+  start_lemma_with_initialization ?hook ~kind evd ~udecl recguard thms snl
 
 (************************************************************************)
 (* Admitting a lemma-like constant                                      *)
@@ -478,7 +486,7 @@ let save_lemma_admitted ?proof ~(lemma : t) =
     let open Proof_global in
     let env = Global.env () in
     match proof with
-    | Some ({ id; entries; persistence = k; universes }, { hook; impargs; udecl; other_thms } ) ->
+    | Some ({ id; entries; persistence = k; universes }, { Info.hook; impargs; udecl; other_thms; _} ) ->
       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
@@ -515,7 +523,7 @@ let save_lemma_admitted ?proof ~(lemma : t) =
             Some (Environ.keep_hyps env (Id.Set.union ids_typ ids_def))
           | _ -> None in
       let udecl = Proof_global.get_universe_decl lemma.proof in
-      let { hook; impargs; other_thms } = lemma.info in
+      let { Info.hook; impargs; other_thms } = lemma.info in
       let { Proof.sigma } = Proof.data (Proof_global.get_proof lemma.proof) in
       let ctx = UState.check_univ_decl ~poly universes udecl in
       finish_admitted env sigma name gk (sec_vars, (typ, ctx), None) universes hook udecl impargs other_thms
@@ -526,7 +534,7 @@ let save_lemma_admitted ?proof ~(lemma : t) =
 
 let finish_proved env sigma opaque idopt po info =
   let open Proof_global in
-  let { hook; compute_guard; udecl; impargs; other_thms } = info in
+  let { Info.hook; compute_guard; udecl; impargs; other_thms } = info in
   match po with
   | { id; entries=[const]; persistence=locality,poly,kind; universes } ->
     let is_opaque = match opaque with
@@ -659,7 +667,7 @@ let save_lemma_proved ?proof ?lemma ~opaque ~idopt =
   in
   let open Proof_global in
   let open Proof_ending in
-  match CEphemeron.default proof_info.proof_ending Regular with
+  match CEphemeron.default proof_info.Info.proof_ending Regular with
   | Regular ->
     finish_proved env sigma opaque idopt proof_obj proof_info
   | End_obligation oinfo ->
diff --git a/vernac/lemmas.mli b/vernac/lemmas.mli
index 9bbb635336..c1a034c30f 100644
--- a/vernac/lemmas.mli
+++ b/vernac/lemmas.mli
@@ -11,9 +11,11 @@
 open Names
 open Decl_kinds
 
-(* Proofs that define a constant *)
+(** {4 Proofs attached to a constant} *)
+
 type t
-type lemma_possible_guards = int list list
+(** [Lemmas.t] represents a constant that is being proved, usually
+    interactively *)
 
 module Stack : sig
 
@@ -40,11 +42,12 @@ end
 val set_endline_tactic : Genarg.glob_generic_argument -> t -> t
 val pf_map : (Proof_global.t -> Proof_global.t) -> t -> t
 val pf_fold : (Proof_global.t -> 'a) -> t -> 'a
+(** [pf_fold f l] fold over the underlying proof object *)
 
 val by : unit Proofview.tactic -> t -> t * bool
+(** [by tac l] apply a tactic to [l] *)
 
-(* Start of high-level proofs with an associated constant *)
-
+(** Creating high-level proofs with an associated constant *)
 module Proof_ending : sig
 
   type t =
@@ -69,44 +72,51 @@ module Recthm : sig
     ; args : Name.t list
     (** Names to pre-introduce  *)
     ; impargs : Impargs.manual_implicits
+    (** Explicitily declared implicit arguments  *)
     }
 end
 
+module Info : sig
+
+  type t
+
+  val make
+    :  ?hook: DeclareDef.Hook.t
+    (** Callback to be executed at the end of the proof *)
+    -> ?udecl : UState.universe_decl
+    (** Universe declaration *)
+    -> ?proof_ending : Proof_ending.t
+    (** Info for special constants *)
+    -> unit
+    -> t
+
+end
+
+(** Starts the proof of a constant *)
 val start_lemma
-  :  Id.t
-  -> ?udecl:UState.universe_decl
-  -> goal_kind
-  -> Evd.evar_map
-  -> ?proof_ending:Proof_ending.t
+  :  name:Id.t
+  -> kind:goal_kind
   -> ?sign:Environ.named_context_val
-  -> ?compute_guard:lemma_possible_guards
-  -> ?hook:DeclareDef.Hook.t
-  -> ?impargs:Impargs.manual_implicits
-  -> ?other_thms:Recthm.t list
+  -> ?info:Info.t
+  -> Evd.evar_map
   -> EConstr.types
   -> t
 
 val start_dependent_lemma
-  :  Id.t
-  -> ?udecl:UState.universe_decl
-  -> goal_kind
-  -> ?proof_ending:Proof_ending.t
-  -> ?compute_guard:lemma_possible_guards
-  -> ?hook:DeclareDef.Hook.t
-  -> ?impargs:Impargs.manual_implicits
-  -> ?other_thms:Recthm.t list
+  :  name:Id.t
+  -> kind:goal_kind
+  -> ?info:Info.t
   -> Proofview.telescope
   -> t
 
-val start_lemma_com
-  :  program_mode:bool
-  -> ?inference_hook:Pretyping.inference_hook
-  -> ?hook:DeclareDef.Hook.t -> goal_kind -> Vernacexpr.proof_expr list
-  -> t
+type lemma_possible_guards = int list list
 
+(** Pretty much internal, only used in ComFixpoint *)
 val start_lemma_with_initialization
   :  ?hook:DeclareDef.Hook.t
-  -> goal_kind -> Evd.evar_map -> UState.universe_decl
+  -> kind:goal_kind
+  -> udecl:UState.universe_decl
+  -> Evd.evar_map
   -> (bool * lemma_possible_guards * unit Proofview.tactic list option) option
   -> Recthm.t list
   -> int list option
@@ -114,31 +124,43 @@ val start_lemma_with_initialization
 
 val default_thm_id : Names.Id.t
 
+(** Main [Lemma foo args : type.] command *)
+val start_lemma_com
+  :  program_mode:bool
+  -> kind:goal_kind
+  -> ?inference_hook:Pretyping.inference_hook
+  -> ?hook:DeclareDef.Hook.t
+  -> Vernacexpr.proof_expr list
+  -> t
+
 (* Prepare global named context for proof session: remove proofs of
    opaque section definitions and remove vm-compiled code *)
 
 val initialize_named_context_for_proof : unit -> Environ.named_context_val
 
-(** {6 Saving proofs } *)
+(** {4 Saving proofs} *)
+
+(** The extra [?proof] parameter here is due to problems with the
+    lower-level [Proof_global.close_proof] API; we cannot inject closed
+    proofs properly in the proof state so we must leave this backdoor open.
 
-type lemma_info
-val default_lemma_info : lemma_info
+    The regular user can ignore it.
+*)
 
 val save_lemma_admitted
-  :  ?proof:(Proof_global.proof_object * lemma_info)
+  :  ?proof:(Proof_global.proof_object * Info.t)
   -> lemma:t
   -> unit
 
 val save_lemma_proved
-  :  ?proof:(Proof_global.proof_object * lemma_info)
+  :  ?proof:(Proof_global.proof_object * Info.t)
   -> ?lemma:t
   -> opaque:Proof_global.opacity_flag
   -> idopt:Names.lident option
   -> unit
 
-(* To be removed *)
+(** To be removed, don't use! *)
 module Internal : sig
+  val get_info : t -> Info.t
   (** Only needed due to the Proof_global compatibility layer. *)
-  val get_info : t -> lemma_info
-
 end
diff --git a/vernac/obligations.ml b/vernac/obligations.ml
index aa15718452..4e4f80fd71 100644
--- a/vernac/obligations.ml
+++ b/vernac/obligations.ml
@@ -492,7 +492,8 @@ let rec solve_obligation prg num tac =
   let auto n oblset tac = auto_solve_obligations n ~oblset tac in
   let proof_ending = Lemmas.Proof_ending.End_obligation (DeclareObl.{name = prg.prg_name; num; auto}) in
   let hook = DeclareDef.Hook.make (obligation_hook prg obl num auto) in
-  let lemma = Lemmas.start_lemma ~sign:prg.prg_sign obl.obl_name kind evd (EConstr.of_constr obl.obl_type) ~proof_ending ~hook in
+  let info = Lemmas.Info.make ~hook ~proof_ending () in
+  let lemma = Lemmas.start_lemma ~sign:prg.prg_sign ~name:obl.obl_name ~kind ~info evd (EConstr.of_constr obl.obl_type) in
   let lemma = fst @@ Lemmas.by !default_tactic lemma in
   let lemma = Option.cata (fun tac -> Lemmas.set_endline_tactic tac lemma) lemma tac in
   lemma
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 222f727f8e..da8808ccaa 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -582,7 +582,7 @@ let start_proof_and_print ~program_mode ?hook k l =
       in Some hook
     else None
   in
-  start_lemma_com ~program_mode ?inference_hook ?hook k l
+  start_lemma_com ~program_mode ?inference_hook ?hook ~kind:k l
 
 let vernac_definition_hook p = function
 | Coercion ->
diff --git a/vernac/vernacentries.mli b/vernac/vernacentries.mli
index 05de191214..ad3e9f93d9 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.lemma_info) ->
+  ?proof:(Proof_global.proof_object * Lemmas.Info.t) ->
   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 eabbb78d47..f9b4aec45e 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.lemma_info
+  type closed_proof = Proof_global.proof_object * Lemmas.Info.t
 
 
   let return_proof ?allow_partial () = cc (return_proof ?allow_partial)
diff --git a/vernac/vernacstate.mli b/vernac/vernacstate.mli
index 1d292077da..5234ef7a73 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.lemma_info
+  type closed_proof = Proof_global.proof_object * Lemmas.Info.t
 
   val close_future_proof :
     opaque:Proof_global.opacity_flag ->