From d65eaaaa8cb311a0344a584df7a4b405034780b9 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Tue, 24 Mar 2015 15:56:51 +0100
Subject: Revert "Useless check when loading notations through import."

This reverts commit 124734fd2c523909802d095abb37350519856864.
---
 interp/notation.ml     | 8 ++++++++
 interp/notation.mli    | 4 ++++
 toplevel/metasyntax.ml | 2 +-
 3 files changed, 13 insertions(+), 1 deletion(-)

diff --git a/interp/notation.ml b/interp/notation.ml
index aeec4b6153..6040c33a5e 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -516,6 +516,14 @@ let availability_of_prim_token n printer_scope local_scopes =
 
 (* Miscellaneous *)
 
+let exists_notation_in_scope scopt ntn r =
+  let scope = match scopt with Some s -> s | None -> default_scope in
+  try
+    let sc = String.Map.find scope !scope_map in
+    let (r',_) = String.Map.find ntn sc.notations in
+    Pervasives.(=) r' r (** FIXME *)
+  with Not_found -> false
+
 let isNVar_or_NHole = function NVar _ | NHole _ -> true | _ -> false
 
 (**********************************************************************)
diff --git a/interp/notation.mli b/interp/notation.mli
index c66115cbdd..854c52b2c7 100644
--- a/interp/notation.mli
+++ b/interp/notation.mli
@@ -140,6 +140,10 @@ val level_of_notation : notation -> level (** raise [Not_found] if no level *)
 val interp_notation_as_global_reference : Loc.t -> (global_reference -> bool) ->
       notation -> delimiters option -> global_reference
 
+(** Checks for already existing notations *)
+val exists_notation_in_scope : scope_name option -> notation ->
+      interpretation -> bool
+
 (** Declares and looks for scopes associated to arguments of a global ref *)
 val declare_arguments_scope :
   bool (** true=local *) -> global_reference -> scope_name option list -> unit
diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml
index cdbff17149..c8eff59b15 100644
--- a/toplevel/metasyntax.ml
+++ b/toplevel/metasyntax.ml
@@ -1118,7 +1118,7 @@ let open_notation i (_, nobj) =
   let scope = nobj.notobj_scope in
   let (ntn, df) = nobj.notobj_notation in
   let pat = nobj.notobj_interp in
-  if Int.equal i 1 then begin
+  if Int.equal i 1 && not (Notation.exists_notation_in_scope scope ntn pat) then begin
     (* Declare the interpretation *)
     Notation.declare_notation_interpretation ntn scope pat df;
     (* Declare the uninterpretation *)
-- 
cgit v1.2.3