[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, 7 insertions, 0 deletions

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 ++