[declare] Remove mutual internals from Info.t structure.

We move the advanced proof initialization routine to Declare, and stop
exposing implementation internals in `Info.t` constructor.

8 files changed, 69 insertions, 74 deletions

diff --git a/proofs/proof.ml b/proofs/proof.ml
index 175c487958..a183fa7797 100644
--- a/proofs/proof.ml
+++ b/proofs/proof.ml
@@ -120,7 +120,7 @@ type t =
   ; name : Names.Id.t
   (** the name of the theorem whose proof is being constructed *)
   ; poly : bool
-  (** Locality, polymorphism, and "kind" [Coercion, Definition, etc...] *)
+  (** polymorphism *)
   }
 
 (*** General proof functions ***)
diff --git a/vernac/comFixpoint.ml b/vernac/comFixpoint.ml
index 2995df4a66..5bf3350777 100644
--- a/vernac/comFixpoint.ml
+++ b/vernac/comFixpoint.ml
@@ -271,7 +271,7 @@ let declare_fixpoint_interactive_generic ?indexes ~scope ~poly ((fixnames,_fixrs
   let init_terms = Some fixdefs in
   let evd = Evd.from_ctx ctx in
   let lemma =
-    Lemmas.start_lemma_with_initialization ~poly ~scope ~kind:(Decls.IsDefinition fix_kind) ~udecl
+    Declare.start_proof_with_initialization ~poly ~scope ~kind:(Decls.IsDefinition fix_kind) ~udecl
       evd (Some(cofix,indexes,init_terms)) thms None in
   (* Declare notations *)
   List.iter (Metasyntax.add_notation_interpretation (Global.env())) ntns;
diff --git a/vernac/declare.ml b/vernac/declare.ml
index b2f46c2a83..ebea919f64 100644
--- a/vernac/declare.ml
+++ b/vernac/declare.ml
@@ -97,11 +97,11 @@ module Info = struct
     }
 
   let make ?hook ?(proof_ending=Proof_ending.Regular) ?(scope=Locality.Global Locality.ImportDefaultBehavior)
-      ?(kind=Decls.(IsProof Lemma)) ?(compute_guard=[]) ?(thms=[]) () =
+      ?(kind=Decls.(IsProof Lemma)) () =
     { hook
-    ; compute_guard
+    ; compute_guard = []
     ; proof_ending = CEphemeron.create proof_ending
-    ; thms
+    ; thms = []
     ; scope
     ; kind
     }
@@ -205,6 +205,50 @@ let start_dependent_proof ~name ~udecl ~poly ~info goals =
   ; info
   }
 
+let rec_tac_initializer finite guard thms snl =
+  if finite then
+    match List.map (fun { Recthm.name; typ } -> name, (EConstr.of_constr 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
+     | None -> List.map succ (List.map List.last guard)
+     | Some nl -> nl
+    in match List.map2 (fun { Recthm.name; typ } n -> (name, n, (EConstr.of_constr typ))) thms nl with
+       | (id,n,_)::l -> Tactics.mutual_fix id n l 0
+       | _ -> assert false
+
+let start_proof_with_initialization ?hook ~poly ~scope ~kind ~udecl sigma recguard thms snl =
+  let intro_tac { Recthm.args; _ } = Tactics.auto_intros_tac args in
+  let init_tac, compute_guard = match recguard with
+  | Some (finite,guard,init_terms) ->
+    let rec_tac = rec_tac_initializer finite guard thms snl in
+    let term_tac =
+      match init_terms with
+      | None ->
+        List.map intro_tac thms
+      | Some init_terms ->
+        (* This is the case for hybrid proof mode / definition
+           fixpoint, where terms for some constants are given with := *)
+        let tacl = List.map (Option.cata (EConstr.of_constr %> Tactics.exact_no_check) Tacticals.New.tclIDTAC) init_terms in
+        List.map2 (fun tac thm -> Tacticals.New.tclTHEN tac (intro_tac thm)) tacl thms
+    in
+    Tacticals.New.tclTHENS rec_tac term_tac, guard
+  | None ->
+    let () = match thms with [_] -> () | _ -> assert false in
+    intro_tac (List.hd thms), [] in
+  match thms with
+  | [] -> CErrors.anomaly (Pp.str "No proof to start.")
+  | { Recthm.name; typ; impargs; _} :: thms ->
+    let info = Info.make ?hook ~scope ~kind () in
+    let info = { info with Info.compute_guard; thms } in
+    (* start_lemma has the responsibility to add (name, impargs, typ)
+       to thms, once Info.t is more refined this won't be necessary *)
+    let lemma = start_proof ~name ~impargs ~poly ~udecl ~info sigma (EConstr.of_constr typ) in
+    map_proof (fun p ->
+        pi1 @@ Proof.run_tactic Global.(env ()) init_tac p) lemma
+
 let get_used_variables pf = pf.section_vars
 let get_universe_decl pf = pf.udecl
 
@@ -2039,5 +2083,5 @@ module Proof = struct
   let compact = compact_the_proof
   let update_global_env = update_global_env
   let get_open_goals = get_open_goals
-  let get_info { info } = info
+  let info { info } = info
 end
diff --git a/vernac/declare.mli b/vernac/declare.mli
index ef35628de2..55c6175371 100644
--- a/vernac/declare.mli
+++ b/vernac/declare.mli
@@ -121,10 +121,6 @@ module Info : sig
     (** locality  *)
     -> ?kind:Decls.logical_kind
     (** Theorem, etc... *)
-    -> ?compute_guard:lemma_possible_guards
-    -> ?thms:Recthm.t list
-    (** Both of those are internal, used by the upper layers but will
-       become handled natively here in the future *)
     -> unit
     -> t
 
@@ -163,7 +159,7 @@ module Proof : sig
   val get_open_goals : t -> int
 
   (* Internal, don't use *)
-  val get_info : t -> Info.t
+  val info : t -> Info.t
 end
 
 type opacity_flag = Vernacexpr.opacity_flag = Opaque | Transparent
@@ -194,6 +190,19 @@ val start_dependent_proof
   -> Proofview.telescope
   -> Proof.t
 
+(** Pretty much internal, used by the Lemma / Fixpoint vernaculars *)
+val start_proof_with_initialization
+  :  ?hook:Hook.t
+  -> poly:bool
+  -> scope:Locality.locality
+  -> kind:Decls.logical_kind
+  -> udecl:UState.universe_decl
+  -> Evd.evar_map
+  -> (bool * lemma_possible_guards * Constr.t option list option) option
+  -> Recthm.t list
+  -> int list option
+  -> Proof.t
+
 (** Proof entries represent a proof that has been finished, but still
    not registered with the kernel.
 
diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml
index 450699a1e8..6fe9b7c257 100644
--- a/vernac/lemmas.ml
+++ b/vernac/lemmas.ml
@@ -11,8 +11,6 @@
 (* Created by Hugo Herbelin from contents related to lemma proofs in
    file command.ml, Aug 2009 *)
 
-open Util
-
 (************************************************************************)
 (* Creating a lemma-like constant                                       *)
 (************************************************************************)
@@ -30,46 +28,3 @@ let start_dependent_lemma ~name ~poly
     ?(udecl=UState.default_univ_decl)
     ?(info=Declare.Info.make ()) telescope =
   Declare.start_dependent_proof ~name ~udecl ~poly ~info telescope
-
-let rec_tac_initializer finite guard thms snl =
-  if finite then
-    match List.map (fun { Declare.Recthm.name; typ } -> name, (EConstr.of_constr 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
-     | None -> List.map succ (List.map List.last guard)
-     | Some nl -> nl
-    in match List.map2 (fun { Declare.Recthm.name; typ } n -> (name, n, (EConstr.of_constr typ))) thms nl with
-       | (id,n,_)::l -> Tactics.mutual_fix id n l 0
-       | _ -> assert false
-
-let start_lemma_with_initialization ?hook ~poly ~scope ~kind ~udecl sigma recguard thms snl =
-  let intro_tac { Declare.Recthm.args; _ } = Tactics.auto_intros_tac args in
-  let init_tac, compute_guard = match recguard with
-  | Some (finite,guard,init_terms) ->
-    let rec_tac = rec_tac_initializer finite guard thms snl in
-    let term_tac =
-      match init_terms with
-      | None ->
-        List.map intro_tac thms
-      | Some init_terms ->
-        (* This is the case for hybrid proof mode / definition
-           fixpoint, where terms for some constants are given with := *)
-        let tacl = List.map (Option.cata (EConstr.of_constr %> Tactics.exact_no_check) Tacticals.New.tclIDTAC) init_terms in
-        List.map2 (fun tac thm -> Tacticals.New.tclTHEN tac (intro_tac thm)) tacl thms
-    in
-    Tacticals.New.tclTHENS rec_tac term_tac, guard
-  | None ->
-    let () = match thms with [_] -> () | _ -> assert false in
-    intro_tac (List.hd thms), [] in
-  match thms with
-  | [] -> CErrors.anomaly (Pp.str "No proof to start.")
-  | { Declare.Recthm.name; typ; impargs; _} :: thms ->
-    let info = Declare.Info.make ?hook ~scope ~kind ~compute_guard ~thms () in
-    (* start_lemma has the responsibility to add (name, impargs, typ)
-       to thms, once Info.t is more refined this won't be necessary *)
-    let lemma = start_lemma ~name ~impargs ~poly ~udecl ~info sigma (EConstr.of_constr typ) in
-    Declare.Proof.map ~f:(fun p ->
-        pi1 @@ Proof.run_tactic Global.(env ()) init_tac p) lemma
diff --git a/vernac/lemmas.mli b/vernac/lemmas.mli
index f882854862..ef89b9e1ee 100644
--- a/vernac/lemmas.mli
+++ b/vernac/lemmas.mli
@@ -30,16 +30,3 @@ val start_dependent_lemma
   -> ?info:Declare.Info.t
   -> Proofview.telescope
   -> Declare.Proof.t
-
-(** Pretty much internal, used by the Lemma / Fixpoint vernaculars *)
-val start_lemma_with_initialization
-  :  ?hook:Declare.Hook.t
-  -> poly:bool
-  -> scope:Declare.locality
-  -> kind:Decls.logical_kind
-  -> udecl:UState.universe_decl
-  -> Evd.evar_map
-  -> (bool * Declare.lemma_possible_guards * Constr.t option list option) option
-  -> Declare.Recthm.t list
-  -> int list option
-  -> Declare.Proof.t
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index a3dd1856aa..1ada477d07 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -521,7 +521,7 @@ let start_lemma_com ~program_mode ~poly ~scope ~kind ?hook thms =
     else (* We fix the variables to ensure they won't be lowered to Set *)
       Evd.fix_undefined_variables evd
   in
-  Lemmas.start_lemma_with_initialization ?hook ~poly ~scope ~kind evd ~udecl recguard thms snl
+  Declare.start_proof_with_initialization ?hook ~poly ~scope ~kind evd ~udecl recguard thms snl
 
 let vernac_definition_hook ~canonical_instance ~local ~poly = let open Decls in function
 | Coercion ->
diff --git a/vernac/vernacstate.ml b/vernac/vernacstate.ml
index 5968e6a982..536f413bf4 100644
--- a/vernac/vernacstate.ml
+++ b/vernac/vernacstate.ml
@@ -48,9 +48,9 @@ module LemmaStack = struct
     pn :: pns
 
   let copy_info src tgt =
-    Declare.Proof.map ~f:(fun _ -> Declare.Proof.fold ~f:(fun x -> x) tgt) src
+    Declare.Proof.map ~f:(fun _ -> Declare.Proof.get tgt) src
 
-  let copy_info ~src ~tgt =
+  let copy_info ~(src : t) ~(tgt : t) =
     let (ps, psl), (ts,tsl) = src, tgt in
     copy_info ps ts,
     List.map2 (fun op p -> copy_info op p) psl tsl
@@ -160,11 +160,11 @@ module Declare = struct
 
   let close_future_proof ~feedback_id pf =
     cc (fun pt -> Declare.close_future_proof ~feedback_id pt pf,
-                  Declare.Proof.get_info pt)
+                  Declare.Proof.info pt)
 
   let close_proof ~opaque ~keep_body_ucst_separate =
     cc (fun pt -> Declare.close_proof ~opaque ~keep_body_ucst_separate pt,
-                  Declare.Proof.get_info pt)
+                  Declare.Proof.info pt)
 
   let discard_all () = s_lemmas := None
   let update_global_env () = dd (Declare.Proof.update_global_env)