[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.

1 files changed, 2 insertions, 4 deletions

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;