[declare] Use Recthm.t in mutual analysis functions

This removes so ad-hoc tuples, and encapsulates the API a bit.

It is a step towards:

- Pushing some `to_constr` from the upper layers to the declare code
  itself [which will remove code duplication, in particular making the
  interactive / non-interactive path more uniform, and make the API
  easier to use]

- Further refactoring of the constant information, as `Recthm.t`
  contains almost now what we would call "primitive constant
  information"; thus we will be able to distinguish next better between
  mutual declarations and single-constant ones.

6 files changed, 35 insertions, 26 deletions

diff --git a/vernac/declare.ml b/vernac/declare.ml
index e9735eeb7d..5a55757d34 100644
--- a/vernac/declare.ml
+++ b/vernac/declare.ml
@@ -69,16 +69,20 @@ end
 type lemma_possible_guards = int list list
 
 module Recthm = struct
-  type t =
+
+  type 'constr t =
     { name : Names.Id.t
     (** Name of theorem *)
-    ; typ : Constr.t
+    ; typ : 'constr
     (** Type of theorem  *)
     ; args : Names.Name.t list
     (** Names to pre-introduce  *)
     ; impargs : Impargs.manual_implicits
     (** Explicitily declared implicit arguments  *)
     }
+
+  let to_constr sigma thm = { thm with typ = EConstr.to_constr sigma thm.typ }
+
 end
 
 module Info = struct
@@ -91,7 +95,7 @@ module Info = struct
     ; kind : Decls.logical_kind
     ; udecl: UState.universe_decl
     (** Initial universe declarations *)
-    ; thms : Recthm.t list
+    ; thms : Constr.t Recthm.t list
     (** thms contains each individual constant info in a mutual decl *)
     ; compute_guard : lemma_possible_guards
     (** thms and compute guard are specific only to
diff --git a/vernac/declare.mli b/vernac/declare.mli
index 386635cb3f..84f065b134 100644
--- a/vernac/declare.mli
+++ b/vernac/declare.mli
@@ -113,16 +113,20 @@ val declare_assumption
   -> GlobRef.t
 
 module Recthm : sig
-  type t =
+  type 'constr t =
     { name : Id.t
     (** Name of theorem *)
-    ; typ : Constr.t
+    ; typ : 'constr
     (** Type of theorem  *)
     ; args : Name.t list
     (** Names to pre-introduce  *)
     ; impargs : Impargs.manual_implicits
     (** Explicitily declared implicit arguments  *)
     }
+
+  (* Eventually we would like to remove the constr parameter *)
+  val to_constr : Evd.evar_map -> EConstr.t t -> Constr.t t
+
 end
 
 type lemma_possible_guards = int list list
@@ -133,7 +137,7 @@ val declare_mutually_recursive
   -> uctx:UState.t
   -> rec_declaration:Constr.rec_declaration
   -> possible_indexes:lemma_possible_guards option
-  -> Recthm.t list
+  -> Constr.t Recthm.t list
   -> Names.GlobRef.t list
 
 (** {2 Declaration of interactive constants }  *)
@@ -221,7 +225,7 @@ module Proof : sig
     -> kind:Decls.logical_kind
     -> udecl:UState.universe_decl
     -> Evd.evar_map
-    -> Recthm.t
+    -> Constr.t Recthm.t
     -> t
 
   type mutual_info = (bool * lemma_possible_guards * Constr.t option list option)
@@ -235,7 +239,7 @@ module Proof : sig
     -> udecl:UState.universe_decl
     -> Evd.evar_map
     -> mutual_info:mutual_info
-    -> Recthm.t list
+    -> Constr.t Recthm.t list
     -> int list option
     -> t
 
diff --git a/vernac/obligations.mli b/vernac/obligations.mli
index a3e0d3b5c1..ee6a9a17bb 100644
--- a/vernac/obligations.mli
+++ b/vernac/obligations.mli
@@ -87,7 +87,7 @@ val add_definition :
 (** Start a [Program Fixpoint] declaration, similar to the above,
    except it takes a list now. *)
 val add_mutual_definitions :
-     (Declare.Recthm.t * Constr.t * RetrieveObl.obligation_info) list
+     (Constr.t Declare.Recthm.t * Constr.t * RetrieveObl.obligation_info) list
   -> uctx:UState.t
   -> ?udecl:UState.universe_decl (** Universe binders and constraints *)
   -> ?tactic:unit Proofview.tactic
diff --git a/vernac/recLemmas.ml b/vernac/recLemmas.ml
index 797eaa7202..c08fdf8b96 100644
--- a/vernac/recLemmas.ml
+++ b/vernac/recLemmas.ml
@@ -16,9 +16,8 @@ module RelDecl = Context.Rel.Declaration
 
 let find_mutually_recursive_statements sigma thms =
     let n = List.length thms in
-    let inds = List.map (fun (id,t,args,impls) ->
-      let (hyps,ccl) = EConstr.decompose_prod_assum sigma t in
-      let x = (id,t,args,impls) in
+    let inds = List.map (fun ({ Declare.Recthm.name; typ; args; impargs} as x) ->
+      let (hyps,ccl) = EConstr.decompose_prod_assum sigma typ in
       let whnf_hyp_hds = EConstr.map_rel_context_in_env
         (fun env c -> fst (Reductionops.whd_all_stack env sigma c))
         (Global.env()) hyps in
@@ -90,18 +89,18 @@ let find_mutually_recursive_statements sigma thms =
     (finite,guard,None), ordered_inds
 
 type mutual_info =
-  | NonMutual of Names.Id.t * EConstr.t * Names.Name.t list * Impargs.manual_implicits
+  | NonMutual of EConstr.t Declare.Recthm.t
   | Mutual of
-      { mutual_info : bool * int list list * Constr.t option list option
-      ; thms : (Names.Id.t * EConstr.t * Names.Name.t list * Impargs.manual_implicits) list
+      { mutual_info : Declare.Proof.mutual_info
+      ; thms : EConstr.t Declare.Recthm.t list
       ; possible_guards : int list
       }
 
 let look_for_possibly_mutual_statements sigma thms : mutual_info =
   match thms with
-  | [id,t,args,impls] ->
+  | [thm] ->
       (* One non recursively proved theorem *)
-    NonMutual (id,t,args,impls)
+    NonMutual thm
   | _::_ as thms ->
     (* More than one statement and/or an explicit decreasing mark: *)
     (* we look for a common inductive hyp or a common coinductive conclusion *)
diff --git a/vernac/recLemmas.mli b/vernac/recLemmas.mli
index 0d297ca9b9..64890962ba 100644
--- a/vernac/recLemmas.mli
+++ b/vernac/recLemmas.mli
@@ -9,14 +9,14 @@
 (************************************************************************)
 
 type mutual_info =
-  | NonMutual of Names.Id.t * EConstr.t * Names.Name.t list * Impargs.manual_implicits
+  | NonMutual of EConstr.t Declare.Recthm.t
   | Mutual of
-      { mutual_info : bool * int list list * Constr.t option list option
-      ; thms : (Names.Id.t * EConstr.t * Names.Name.t list * Impargs.manual_implicits) list
+      { mutual_info : Declare.Proof.mutual_info
+      ; thms : EConstr.t Declare.Recthm.t list
       ; possible_guards : int list
       }
 
 val look_for_possibly_mutual_statements
   :  Evd.evar_map
-  -> (Names.Id.t * EConstr.t * Names.Name.t list * Impargs.manual_implicits) list
+  -> EConstr.t Declare.Recthm.t list
   -> mutual_info
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 650fc00e88..cbf43127ca 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -515,18 +515,20 @@ let start_lemma_com ~program_mode ~poly ~scope ~kind ?hook thms =
     let evd = Pretyping.solve_remaining_evars ?hook:inference_hook flags env evd in
     let ids = List.map Context.Rel.Declaration.get_name ctx in
     check_name_freshness scope id;
-    evd, (id.CAst.v, EConstr.it_mkProd_or_LetIn t' ctx, ids, imps @ imps'))
+    let thm = { Declare.Recthm.name = id.CAst.v
+              ; typ = EConstr.it_mkProd_or_LetIn t' ctx
+              ; args = ids; impargs = imps @ imps' } in
+    evd, thm)
       evd thms in
   let mut_analysis = RecLemmas.look_for_possibly_mutual_statements evd thms in
   let evd = Evd.minimize_universes evd in
   match mut_analysis with
-  | RecLemmas.NonMutual (name, typ, args, impargs) ->
-    let thm = { Declare.Recthm.name; typ = EConstr.to_constr evd typ; args; impargs } in
+  | RecLemmas.NonMutual thm ->
+    let thm = Declare.Recthm.to_constr evd thm in
     let evd = post_check_evd ~udecl ~poly evd in
     Declare.Proof.start_with_initialization ?hook ~poly ~scope ~kind evd ~udecl thm
   | RecLemmas.Mutual { mutual_info; thms ; possible_guards } ->
-    let thms = List.map (fun (name, typ, args, impargs) ->
-        { Declare.Recthm.name; typ = EConstr.to_constr evd typ; args; impargs} ) thms in
+    let thms = List.map (Declare.Recthm.to_constr evd) thms in
     let evd = post_check_evd ~udecl ~poly evd in
     Declare.Proof.start_mutual_with_initialization ?hook ~poly ~scope ~kind evd ~udecl ~mutual_info thms (Some possible_guards)