[proof] [mutual] Factorize mutual per-entry information

We move `Recthm` to `DeclareDef` so it is shared by interactive and
direct fixpoint declaration.

This is the last step before unifying both paths.

7 files changed, 70 insertions, 60 deletions

diff --git a/vernac/comFixpoint.ml b/vernac/comFixpoint.ml
index 0e2d8c1453..6580495295 100644
--- a/vernac/comFixpoint.ml
+++ b/vernac/comFixpoint.ml
@@ -236,16 +236,22 @@ let interp_fixpoint ~cofix l =
   let uctx,fix = ground_fixpoint env evd fix in
   (fix,pl,uctx,info)
 
-let declare_fixpoint_interactive_generic ?indexes ~scope ~poly ((fixnames,_fixrs,fixdefs,fixtypes),udecl,ctx,fiximps) ntns =
-  let fix_kind, cofix, indexes = match indexes with
-    | Some indexes -> Decls.Fixpoint, false, indexes
-    | None -> Decls.CoFixpoint, true, []
+let build_recthms ~indexes fixnames fixtypes fiximps =
+  let fix_kind, cofix = match indexes with
+    | Some indexes -> Decls.Fixpoint, false
+    | None -> Decls.CoFixpoint, true
   in
   let thms =
     List.map3 (fun name typ (ctx,impargs,_) ->
-        { Lemmas.Recthm.name; typ
+        { DeclareDef.Recthm.name; typ
         ; args = List.map Context.Rel.Declaration.get_name ctx; impargs})
-      fixnames fixtypes fiximps in
+      fixnames fixtypes fiximps
+  in
+  fix_kind, cofix, thms
+
+let declare_fixpoint_interactive_generic ?indexes ~scope ~poly ((fixnames,_fixrs,fixdefs,fixtypes),udecl,ctx,fiximps) ntns =
+  let fix_kind, cofix, thms = build_recthms ~indexes fixnames fixtypes fiximps in
+  let indexes = Option.default [] indexes in
   let init_terms = Some fixdefs in
   let evd = Evd.from_ctx ctx in
   let lemma =
@@ -256,19 +262,15 @@ let declare_fixpoint_interactive_generic ?indexes ~scope ~poly ((fixnames,_fixrs
   lemma
 
 let declare_fixpoint_generic ?indexes ~scope ~poly ((fixnames,fixrs,fixdefs,fixtypes),udecl,uctx,fiximps) ntns =
-  let possible_indexes, fix_kind =
-    match indexes with
-    | Some indexes -> Some indexes, Decls.(IsDefinition Fixpoint)
-    | None -> None, Decls.(IsDefinition CoFixpoint)
-  in
   (* We shortcut the proof process *)
+  let fix_kind, cofix, fixitems = build_recthms ~indexes fixnames fixtypes fiximps in
   let fixdefs = List.map Option.get fixdefs in
   let rec_declaration = prepare_recursive_declaration fixnames fixrs fixtypes fixdefs in
-  let fiximps = List.map (fun (n,r,p) -> r) fiximps in
+  let fix_kind = Decls.IsDefinition fix_kind in
   let _ : GlobRef.t list =
     DeclareDef.declare_mutually_recursive ~scope ~opaque:false ~kind:fix_kind ~poly ~uctx
-      ~possible_indexes ~restrict_ucontext:true ~udecl ~ntns ~rec_declaration
-      fixnames fixtypes fiximps
+      ~possible_indexes:indexes ~restrict_ucontext:true ~udecl ~ntns ~rec_declaration
+      fixitems
   in
   ()
 
diff --git a/vernac/declareDef.ml b/vernac/declareDef.ml
index de7223ae62..6e19cf97b0 100644
--- a/vernac/declareDef.ml
+++ b/vernac/declareDef.ml
@@ -69,22 +69,35 @@ let declare_definition ~name ~scope ~kind ?hook_data ~ubind ~impargs ce =
   end;
   dref
 
-let mutual_make_bodies ~fixnames ~rec_declaration ~possible_indexes =
+let mutual_make_bodies ~fixitems ~rec_declaration ~possible_indexes =
   match possible_indexes with
   | Some possible_indexes ->
     let env = Global.env() in
     let indexes = Pretyping.search_guard env possible_indexes rec_declaration in
     let vars = Vars.universes_of_constr (Constr.mkFix ((indexes,0),rec_declaration)) in
-    let fixdecls = CList.map_i (fun i _ -> Constr.mkFix ((indexes,i),rec_declaration)) 0 fixnames in
+    let fixdecls = CList.map_i (fun i _ -> Constr.mkFix ((indexes,i),rec_declaration)) 0 fixitems in
     vars, fixdecls, Some indexes
   | None ->
-    let fixdecls = CList.map_i (fun i _ -> Constr.mkCoFix (i,rec_declaration)) 0 fixnames in
+    let fixdecls = CList.map_i (fun i _ -> Constr.mkCoFix (i,rec_declaration)) 0 fixitems in
     let vars = Vars.universes_of_constr (List.hd fixdecls) in
     vars, fixdecls, None
 
-let declare_mutually_recursive ~opaque ~scope ~kind ~poly ~uctx ~udecl ~ntns ~rec_declaration ~possible_indexes ~restrict_ucontext fixnames fixtypes fiximps =
+module Recthm = struct
+  type t =
+    { name : Names.Id.t
+    (** Name of theorem *)
+    ; typ : Constr.t
+    (** Type of theorem  *)
+    ; args : Names.Name.t list
+    (** Names to pre-introduce  *)
+    ; impargs : Impargs.manual_implicits
+    (** Explicitily declared implicit arguments  *)
+    }
+end
+
+let declare_mutually_recursive ~opaque ~scope ~kind ~poly ~uctx ~udecl ~ntns ~rec_declaration ~possible_indexes ~restrict_ucontext fixitems =
   let vars, fixdecls, indexes =
-    mutual_make_bodies ~fixnames ~rec_declaration ~possible_indexes in
+    mutual_make_bodies ~fixitems ~rec_declaration ~possible_indexes in
   let ubind, univs =
     (* XXX: Note that obligations don't do this, is that a bug? *)
     if restrict_ucontext
@@ -97,13 +110,14 @@ let declare_mutually_recursive ~opaque ~scope ~kind ~poly ~uctx ~udecl ~ntns ~re
       let univs = UState.univ_entry ~poly uctx in
       UnivNames.empty_binders, univs
   in
-  let csts = CList.map4
-      (fun name body types impargs ->
-         let ce = Declare.definition_entry ~opaque ~types ~univs body in
+  let csts = CList.map2
+      (fun Recthm.{ name; typ; impargs } body ->
+         let ce = Declare.definition_entry ~opaque ~types:typ ~univs body in
          declare_definition ~name ~scope ~kind ~ubind ~impargs ce)
-      fixnames fixdecls fixtypes fiximps
+      fixitems fixdecls
   in
   let isfix = Option.is_empty possible_indexes in
+  let fixnames = List.map (fun { Recthm.name } -> name) fixitems in
   Declare.recursive_message isfix indexes fixnames;
   List.iter (Metasyntax.add_notation_interpretation (Global.env())) ntns;
   csts
diff --git a/vernac/declareDef.mli b/vernac/declareDef.mli
index 05a38c039d..995aa0ceff 100644
--- a/vernac/declareDef.mli
+++ b/vernac/declareDef.mli
@@ -59,6 +59,19 @@ val declare_assumption
   -> Entries.parameter_entry
   -> GlobRef.t
 
+module Recthm : sig
+  type t =
+    { name : Id.t
+    (** Name of theorem *)
+    ; typ : Constr.t
+    (** Type of theorem  *)
+    ; args : Name.t list
+    (** Names to pre-introduce  *)
+    ; impargs : Impargs.manual_implicits
+    (** Explicitily declared implicit arguments  *)
+    }
+end
+
 val declare_mutually_recursive
   : opaque:bool
   -> scope:locality
@@ -70,9 +83,7 @@ val declare_mutually_recursive
   -> rec_declaration:Constr.rec_declaration
   -> possible_indexes:int list list option
   -> restrict_ucontext:bool
-  -> Names.variable list
-  -> Constr.types list
-  -> Impargs.manual_implicits list
+  -> Recthm.t list
   -> Names.GlobRef.t list
 
 val prepare_definition
diff --git a/vernac/declareObl.ml b/vernac/declareObl.ml
index 95e9a10d03..98a9e4b9c9 100644
--- a/vernac/declareObl.ml
+++ b/vernac/declareObl.ml
@@ -436,7 +436,12 @@ let declare_mutual_definition l =
         (xdef :: defs, xobls @ obls)) l ([], [])
   in
   (*   let fixdefs = List.map reduce_fix fixdefs in *)
-  let fixdefs, fixrs,fixtypes, fiximps = List.split4 defs in
+  let fixdefs, fixrs, fixtypes, fixitems =
+    List.fold_right2 (fun (d,r,typ,impargs) name (a1,a2,a3,a4) ->
+        d :: a1, r :: a2, typ :: a3,
+        DeclareDef.Recthm.{ name; typ; impargs; args = [] } :: a4
+      ) defs first.prg_deps ([],[],[],[])
+  in
   let fixkind = Option.get first.prg_fixkind in
   let arrrec, recvec = (Array.of_list fixtypes, Array.of_list fixdefs) in
   let rvec = Array.of_list fixrs in
@@ -449,14 +454,14 @@ let declare_mutual_definition l =
     | IsCoFixpoint -> None
   in
   (* In the future we will pack all this in a proper record *)
-  let poly, scope, ntns, opaque, fixnames = first.prg_poly, first.prg_scope, first.prg_notations, first.prg_opaque, first.prg_deps in
+  let poly, scope, ntns, opaque = first.prg_poly, first.prg_scope, first.prg_notations, first.prg_opaque in
   let kind = if fixkind != IsCoFixpoint then Decls.(IsDefinition Fixpoint) else Decls.(IsDefinition CoFixpoint) in
   (* Declare the recursive definitions *)
   let udecl = UState.default_univ_decl in
   let kns =
     DeclareDef.declare_mutually_recursive ~scope ~opaque ~kind
-      ~udecl ~ntns ~uctx:first.prg_ctx ~rec_declaration ~possible_indexes
-      ~poly ~restrict_ucontext:false fixnames fixtypes fiximps
+      ~udecl ~ntns ~uctx:first.prg_ctx ~rec_declaration ~possible_indexes ~poly
+      ~restrict_ucontext:false fixitems
   in
   (* Only for the first constant *)
   let fix_exn = Hook.get get_fix_exn () in
diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml
index 7782ff8ac9..7aea40c718 100644
--- a/vernac/lemmas.ml
+++ b/vernac/lemmas.ml
@@ -39,15 +39,6 @@ module Proof_ending = struct
 
 end
 
-module Recthm = struct
-  type t =
-    { name : Id.t
-    ; typ : Constr.t
-    ; args : Name.t list
-    ; impargs : Impargs.manual_implicits
-    }
-end
-
 module Info = struct
 
   type t =
@@ -56,7 +47,7 @@ module Info = struct
     ; impargs : Impargs.manual_implicits
     ; proof_ending : Proof_ending.t CEphemeron.key
     (* This could be improved and the CEphemeron removed *)
-    ; other_thms : Recthm.t list
+    ; other_thms : DeclareDef.Recthm.t list
     ; scope : DeclareDef.locality
     ; kind : Decls.logical_kind
     }
@@ -129,7 +120,7 @@ let start_dependent_lemma ~name ~poly
 
 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
+    match List.map (fun { DeclareDef.Recthm.name; typ } -> name, (EConstr.of_constr typ)) thms with
     | (id,_)::l -> Tactics.mutual_cofix id l 0
     | _ -> assert false
   else
@@ -137,12 +128,12 @@ let rec_tac_initializer finite guard thms snl =
     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
+    in match List.map2 (fun { DeclareDef.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 { Recthm.args; _ } = Tactics.auto_intros_tac args in
+  let intro_tac { DeclareDef.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
@@ -162,7 +153,7 @@ let start_lemma_with_initialization ?hook ~poly ~scope ~kind ~udecl sigma recgua
     intro_tac (List.hd thms), [] in
   match thms with
   | [] -> CErrors.anomaly (Pp.str "No proof to start.")
-  | { Recthm.name; typ; impargs; _}::other_thms ->
+  | { DeclareDef.Recthm.name; typ; impargs; _}::other_thms ->
     let info =
       Info.{ hook
            ; impargs
@@ -290,7 +281,7 @@ end = struct
     let ubind = UnivNames.empty_binders in
     let rs =
       List.map_i (
-        fun i { Recthm.name; typ; impargs } ->
+        fun i { DeclareDef.Recthm.name; typ; impargs } ->
           declare_mutdef ?fix_exn ~name ~info ~ubind ?hook_data ~uctx ~typ ~impargs entry i) 1 info.Info.other_thms
     in r :: rs
 end
diff --git a/vernac/lemmas.mli b/vernac/lemmas.mli
index 471c955311..6a1f8c09f3 100644
--- a/vernac/lemmas.mli
+++ b/vernac/lemmas.mli
@@ -44,19 +44,6 @@ module Proof_ending : sig
 
 end
 
-module Recthm : sig
-  type t =
-    { name : Id.t
-    (** Name of theorem *)
-    ; typ : Constr.t
-    (** Type of theorem  *)
-    ; args : Name.t list
-    (** Names to pre-introduce  *)
-    ; impargs : Impargs.manual_implicits
-    (** Explicitily declared implicit arguments  *)
-    }
-end
-
 module Info : sig
 
   type t
@@ -104,7 +91,7 @@ val start_lemma_with_initialization
   -> udecl:UState.universe_decl
   -> Evd.evar_map
   -> (bool * lemma_possible_guards * Constr.t option list option) option
-  -> Recthm.t list
+  -> DeclareDef.Recthm.t list
   -> int list option
   -> t
 
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index d273573270..8641c67d9f 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -501,7 +501,7 @@ let start_lemma_com ~program_mode ~poly ~scope ~kind ?hook thms =
   let recguard,thms,snl = RecLemmas.look_for_possibly_mutual_statements evd thms in
   let evd = Evd.minimize_universes evd in
   let thms = List.map (fun (name, (typ, (args, impargs))) ->
-      { Lemmas.Recthm.name; typ = EConstr.to_constr evd typ; args; impargs} ) thms in
+      { DeclareDef.Recthm.name; typ = EConstr.to_constr evd typ; args; impargs} ) thms in
   let () =
     let open UState in
     if not (udecl.univdecl_extensible_instance && udecl.univdecl_extensible_constraints) then