1 files changed, 30 insertions, 28 deletions
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;