From 09d6197bd11ed4a323b335118ae749d7caefeb55 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Mon, 9 Mar 2020 01:51:37 -0400
Subject: [proof] [mutual] Factorize notation declaration.

---
 vernac/declareDef.ml | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

(limited to 'vernac/declareDef.ml')

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 =
-- 
cgit v1.2.3