[proof] Start of mutual definition save refactoring.

First commit of a series that will unify (and enforce) the handling of
mutual constants. We will split this in several commits as to easy
debugging / bisect in case of problems.

In this first commit, we move the actual declare logic to a common
place.

6 files changed, 24 insertions, 19 deletions

diff --git a/tactics/proof_global.ml b/tactics/proof_global.ml
index 7fd1634dcf..623e6b8a42 100644
--- a/tactics/proof_global.ml
+++ b/tactics/proof_global.ml
@@ -8,14 +8,6 @@
 (*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
-(***********************************************************************)
-(*                                                                     *)
-(*      This module defines proof facilities relevant to the           *)
-(*      toplevel. In particular it defines the global proof            *)
-(*      environment.                                                   *)
-(*                                                                     *)
-(***********************************************************************)
-
 open Util
 open Names
 open Context
diff --git a/tactics/proof_global.mli b/tactics/proof_global.mli
index f1281d1291..e1c75c0649 100644
--- a/tactics/proof_global.mli
+++ b/tactics/proof_global.mli
@@ -8,9 +8,7 @@
 (*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
-(** This module defines proof facilities relevant to the
-     toplevel. In particular it defines the global proof
-     environment. *)
+(** State for interactive proofs. *)
 
 type t
 
diff --git a/vernac/comFixpoint.ml b/vernac/comFixpoint.ml
index 0a70954dd2..4e5b1d7205 100644
--- a/vernac/comFixpoint.ml
+++ b/vernac/comFixpoint.ml
@@ -279,12 +279,10 @@ let declare_fixpoint_generic ?indexes ~scope ~poly ((fixnames,fixrs,fixdefs,fixt
   let fiximps = List.map (fun (n,r,p) -> r) fiximps in
   let evd = Evd.from_ctx ctx in
   let evd = Evd.restrict_universe_context evd vars in
-  let ctx = Evd.check_univ_decl ~poly evd pl in
+  let univs = Evd.check_univ_decl ~poly evd pl in
   let ubind = Evd.universe_binders evd in
   let _ : GlobRef.t list =
-    List.map4 (fun name body types impargs ->
-        let ce = Declare.definition_entry ~opaque:false ~types ~univs:ctx body in
-        DeclareDef.declare_definition ~name ~scope ~kind:fix_kind ~ubind ~impargs ce)
+    DeclareDef.declare_mutually_recursive ~scope ~opaque:false ~univs ~kind:fix_kind ~ubind
       fixnames fixdecls fixtypes fiximps
   in
   Declare.recursive_message (not cofix) gidx fixnames;
diff --git a/vernac/declareDef.ml b/vernac/declareDef.ml
index 09582f4ef2..edf7ed9dc3 100644
--- a/vernac/declareDef.ml
+++ b/vernac/declareDef.ml
@@ -69,6 +69,13 @@ let declare_definition ~name ~scope ~kind ?hook_data ~ubind ~impargs ce =
   end;
   dref
 
+let declare_mutually_recursive ~opaque ~univs ~scope ~kind ~ubind fixnames fixdecls fixtypes fiximps =
+  CList.map4
+    (fun name body types impargs ->
+       let ce = Declare.definition_entry ~opaque ~types ~univs body in
+       declare_definition ~name ~scope ~kind ~ubind ~impargs ce)
+    fixnames fixdecls fixtypes fiximps
+
 let warn_let_as_axiom =
   CWarnings.create ~name:"let-as-axiom" ~category:"vernacular"
     Pp.(fun id -> strbrk "Let definition" ++ spc () ++ Names.Id.print id ++
diff --git a/vernac/declareDef.mli b/vernac/declareDef.mli
index fb1fc9242c..a62dea05ff 100644
--- a/vernac/declareDef.mli
+++ b/vernac/declareDef.mli
@@ -59,6 +59,18 @@ val declare_assumption
   -> Entries.parameter_entry
   -> GlobRef.t
 
+val declare_mutually_recursive
+  : opaque:bool
+  -> univs:Entries.universes_entry
+  -> scope:locality
+  -> kind:Decls.logical_kind
+  -> ubind:UnivNames.universe_binders
+  -> Names.variable list
+  -> Constr.constr list
+  -> Constr.types list
+  -> Impargs.manual_implicits list
+  -> Names.GlobRef.t list
+
 val prepare_definition
   :  allow_evars:bool
   -> ?opaque:bool
diff --git a/vernac/declareObl.ml b/vernac/declareObl.ml
index c13e884736..bd3f6e2891 100644
--- a/vernac/declareObl.ml
+++ b/vernac/declareObl.ml
@@ -467,10 +467,7 @@ let declare_mutual_definition l =
   let kind = Decls.IsDefinition (if fixkind != IsCoFixpoint then Decls.Fixpoint else Decls.CoFixpoint) in
   let ubind = UnivNames.empty_binders in
   let kns =
-    List.map4
-      (fun name body types impargs ->
-         let ce = Declare.definition_entry ~opaque ~types ~univs body in
-         DeclareDef.declare_definition ~name ~scope ~kind ~ubind ~impargs ce)
+    DeclareDef.declare_mutually_recursive ~scope ~opaque ~univs ~kind ~ubind
       fixnames fixdecls fixtypes fiximps
   in
   (* Declare notations *)
@@ -478,6 +475,7 @@ let declare_mutual_definition l =
     (Metasyntax.add_notation_interpretation (Global.env ()))
     first.prg_notations;
   Declare.recursive_message (fixkind != IsCoFixpoint) indexes fixnames;
+  (* Only for the first constant *)
   let dref = List.hd kns in
   DeclareDef.Hook.(call ?hook:first.prg_hook ~fix_exn { S.uctx = first.prg_ctx; obls; scope; dref });
   List.iter progmap_remove l;