[proof] Factorize call info message in mutual declarations

4 files changed, 16 insertions, 12 deletions

diff --git a/vernac/comFixpoint.ml b/vernac/comFixpoint.ml
index 4e5b1d7205..55ef0f67d6 100644
--- a/vernac/comFixpoint.ml
+++ b/vernac/comFixpoint.ml
@@ -264,7 +264,7 @@ let declare_fixpoint_generic ?indexes ~scope ~poly ((fixnames,fixrs,fixdefs,fixt
   (* We shortcut the proof process *)
   let fixdefs = List.map Option.get fixdefs in
   let fixdecls = prepare_recursive_declaration fixnames fixrs fixtypes fixdefs in
-  let vars, fixdecls, gidx =
+  let vars, fixdecls, indexes =
     if not cofix then
       let env = Global.env() in
       let indexes = Pretyping.search_guard env indexes fixdecls in
@@ -282,10 +282,9 @@ let declare_fixpoint_generic ?indexes ~scope ~poly ((fixnames,fixrs,fixdefs,fixt
   let univs = Evd.check_univ_decl ~poly evd pl in
   let ubind = Evd.universe_binders evd in
   let _ : GlobRef.t list =
-    DeclareDef.declare_mutually_recursive ~scope ~opaque:false ~univs ~kind:fix_kind ~ubind
+    DeclareDef.declare_mutually_recursive ~indexes ~cofix ~scope ~opaque:false ~univs ~kind:fix_kind ~ubind
       fixnames fixdecls fixtypes fiximps
   in
-  Declare.recursive_message (not cofix) gidx fixnames;
   List.iter (Metasyntax.add_notation_interpretation (Global.env())) ntns;
   ()
 
diff --git a/vernac/declareDef.ml b/vernac/declareDef.ml
index edf7ed9dc3..9708f43e53 100644
--- a/vernac/declareDef.ml
+++ b/vernac/declareDef.ml
@@ -69,12 +69,15 @@ 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 declare_mutually_recursive ~cofix ~indexes ~opaque ~univs ~scope ~kind ~ubind fixnames fixdecls fixtypes fiximps =
+  let csts = 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
+  in
+  Declare.recursive_message (not cofix) indexes fixnames;
+  csts
 
 let warn_let_as_axiom =
   CWarnings.create ~name:"let-as-axiom" ~category:"vernacular"
diff --git a/vernac/declareDef.mli b/vernac/declareDef.mli
index a62dea05ff..38a2da4261 100644
--- a/vernac/declareDef.mli
+++ b/vernac/declareDef.mli
@@ -60,7 +60,9 @@ val declare_assumption
   -> GlobRef.t
 
 val declare_mutually_recursive
-  : opaque:bool
+  : cofix:bool
+  -> indexes:int array option
+  -> opaque:bool
   -> univs:Entries.universes_entry
   -> scope:locality
   -> kind:Decls.logical_kind
diff --git a/vernac/declareObl.ml b/vernac/declareObl.ml
index bd3f6e2891..b2d77f4f38 100644
--- a/vernac/declareObl.ml
+++ b/vernac/declareObl.ml
@@ -466,15 +466,15 @@ let declare_mutual_definition l =
   let fix_exn = Hook.get get_fix_exn () in
   let kind = Decls.IsDefinition (if fixkind != IsCoFixpoint then Decls.Fixpoint else Decls.CoFixpoint) in
   let ubind = UnivNames.empty_binders in
+  let cofix = fixkind = IsCoFixpoint in
   let kns =
-    DeclareDef.declare_mutually_recursive ~scope ~opaque ~univs ~kind ~ubind
+    DeclareDef.declare_mutually_recursive ~cofix ~indexes ~scope ~opaque ~univs ~kind ~ubind
       fixnames fixdecls fixtypes fiximps
   in
   (* Declare notations *)
   List.iter
     (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 });