[proof] [mutual] Factorize notation declaration.

4 files changed, 6 insertions, 8 deletions

diff --git a/vernac/comFixpoint.ml b/vernac/comFixpoint.ml
index 55ef0f67d6..ced9656218 100644
--- a/vernac/comFixpoint.ml
+++ b/vernac/comFixpoint.ml
@@ -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 ~indexes ~cofix ~scope ~opaque:false ~univs ~kind:fix_kind ~ubind
+    DeclareDef.declare_mutually_recursive ~indexes ~cofix ~scope ~opaque:false ~univs ~kind:fix_kind ~ubind ~ntns
       fixnames fixdecls fixtypes fiximps
   in
-  List.iter (Metasyntax.add_notation_interpretation (Global.env())) ntns;
   ()
 
 let extract_decreasing_argument ~structonly { CAst.v = v; _ } =
diff --git a/vernac/declareDef.ml b/vernac/declareDef.ml
index 9708f43e53..b3bcf58b4a 100644
--- a/vernac/declareDef.ml
+++ b/vernac/declareDef.ml
@@ -69,7 +69,7 @@ let declare_definition ~name ~scope ~kind ?hook_data ~ubind ~impargs ce =
   end;
   dref
 
-let declare_mutually_recursive ~cofix ~indexes ~opaque ~univs ~scope ~kind ~ubind fixnames fixdecls fixtypes fiximps =
+let declare_mutually_recursive ~cofix ~indexes ~opaque ~univs ~scope ~kind ~ubind ~ntns fixnames fixdecls fixtypes fiximps =
   let csts = CList.map4
       (fun name body types impargs ->
          let ce = Declare.definition_entry ~opaque ~types ~univs body in
@@ -77,6 +77,7 @@ let declare_mutually_recursive ~cofix ~indexes ~opaque ~univs ~scope ~kind ~ubin
       fixnames fixdecls fixtypes fiximps
   in
   Declare.recursive_message (not cofix) indexes fixnames;
+  List.iter (Metasyntax.add_notation_interpretation (Global.env())) ntns;
   csts
 
 let warn_let_as_axiom =
diff --git a/vernac/declareDef.mli b/vernac/declareDef.mli
index 38a2da4261..971f924c6c 100644
--- a/vernac/declareDef.mli
+++ b/vernac/declareDef.mli
@@ -67,6 +67,7 @@ val declare_mutually_recursive
   -> scope:locality
   -> kind:Decls.logical_kind
   -> ubind:UnivNames.universe_binders
+  -> ntns:Vernacexpr.decl_notation list
   -> Names.variable list
   -> Constr.constr list
   -> Constr.types list
diff --git a/vernac/declareObl.ml b/vernac/declareObl.ml
index b2d77f4f38..e530a6e494 100644
--- a/vernac/declareObl.ml
+++ b/vernac/declareObl.ml
@@ -467,14 +467,11 @@ 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 cofix = fixkind = IsCoFixpoint in
+  let ntns = first.prg_notations in
   let kns =
-    DeclareDef.declare_mutually_recursive ~cofix ~indexes ~scope ~opaque ~univs ~kind ~ubind
+    DeclareDef.declare_mutually_recursive ~cofix ~indexes ~scope ~opaque ~univs ~kind ~ubind ~ntns
       fixnames fixdecls fixtypes fiximps
   in
-  (* Declare notations *)
-  List.iter
-    (Metasyntax.add_notation_interpretation (Global.env ()))
-    first.prg_notations;
   (* 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 });