[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.

9 files changed, 117 insertions, 86 deletions

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 ->