Fixing a bug introduced in PR #10832 (new format specific to a given notation).

The import of the format should not be done if i<>1 in open_notation.

2 files changed, 43 insertions, 28 deletions

diff --git a/test-suite/success/Notations2.v b/test-suite/success/Notations2.v
index aa439fae12..b26e725d9b 100644
--- a/test-suite/success/Notations2.v
+++ b/test-suite/success/Notations2.v
@@ -172,3 +172,16 @@ Notation "#" := 0 (only printing).
 Print Visibility.
 
 End Bug10750.
+
+Module M18.
+
+  Module A.
+    Module B.
+    Infix "+++" := Nat.add (at level 70).
+    End B.
+  End A.
+Import A.
+(* Check that the notation in module B is not visible *)
+Infix "+++" := Nat.add (at level 80).
+
+End M18.
diff --git a/vernac/metasyntax.ml b/vernac/metasyntax.ml
index 8f64500996..3644fa4507 100644
--- a/vernac/metasyntax.ml
+++ b/vernac/metasyntax.ml
@@ -1410,34 +1410,36 @@ let load_notation =
   load_notation_common true
 
 let open_notation i (_, nobj) =
-  let scope = nobj.notobj_scope in
-  let (ntn, df) = nobj.notobj_notation in
-  let pat = nobj.notobj_interp in
-  let onlyprint = nobj.notobj_onlyprint  in
-  let deprecation = nobj.notobj_deprecation in
-  let specific = match scope with None -> LastLonelyNotation | Some sc -> NotationInScope sc in
-  let specific_ntn = (specific,ntn) in
-  let fresh = not (Notation.exists_notation_in_scope scope ntn onlyprint pat) in
-  if Int.equal i 1 && fresh then begin
-    (* Declare the interpretation *)
-    let () = Notation.declare_notation_interpretation ntn scope pat df ~onlyprint deprecation in
-    (* Declare the uninterpretation *)
-    if not nobj.notobj_onlyparse then
-      Notation.declare_uninterpretation (NotationRule specific_ntn) pat;
-    (* Declare a possible coercion *)
-    (match nobj.notobj_coercion with
-    | Some (IsEntryCoercion entry) -> Notation.declare_entry_coercion specific_ntn entry
-    | Some (IsEntryGlobal (entry,n)) -> Notation.declare_custom_entry_has_global entry n
-    | Some (IsEntryIdent (entry,n)) -> Notation.declare_custom_entry_has_ident entry n
-    | None -> ())
-  end;
-  (* Declare specific format if any *)
-  match nobj.notobj_specific_pp_rules with
-  | Some pp_sy ->
-    if specific_format_to_declare specific_ntn pp_sy then
-      Ppextend.declare_specific_notation_printing_rules
-        specific_ntn ~extra:pp_sy.synext_extra pp_sy.synext_unparsing
-  | None -> ()
+  if Int.equal i 1 then begin
+    let scope = nobj.notobj_scope in
+    let (ntn, df) = nobj.notobj_notation in
+    let pat = nobj.notobj_interp in
+    let onlyprint = nobj.notobj_onlyprint  in
+    let deprecation = nobj.notobj_deprecation in
+    let specific = match scope with None -> LastLonelyNotation | Some sc -> NotationInScope sc in
+    let specific_ntn = (specific,ntn) in
+    let fresh = not (Notation.exists_notation_in_scope scope ntn onlyprint pat) in
+    if fresh then begin
+      (* Declare the interpretation *)
+      let () = Notation.declare_notation_interpretation ntn scope pat df ~onlyprint deprecation in
+      (* Declare the uninterpretation *)
+      if not nobj.notobj_onlyparse then
+        Notation.declare_uninterpretation (NotationRule specific_ntn) pat;
+      (* Declare a possible coercion *)
+      (match nobj.notobj_coercion with
+      | Some (IsEntryCoercion entry) -> Notation.declare_entry_coercion specific_ntn entry
+      | Some (IsEntryGlobal (entry,n)) -> Notation.declare_custom_entry_has_global entry n
+      | Some (IsEntryIdent (entry,n)) -> Notation.declare_custom_entry_has_ident entry n
+      | None -> ())
+      end;
+    (* Declare specific format if any *)
+    match nobj.notobj_specific_pp_rules with
+    | Some pp_sy ->
+      if specific_format_to_declare specific_ntn pp_sy then
+        Ppextend.declare_specific_notation_printing_rules
+          specific_ntn ~extra:pp_sy.synext_extra pp_sy.synext_unparsing
+    | None -> ()
+  end
 
 let cache_notation o =
   load_notation_common false 1 o;