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 ++++++++
 1 file changed, 8 insertions(+)

(limited to 'interp/notation.ml')

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
 
 (**********************************************************************)
-- 
cgit v1.2.3


From 7c044bd9b5bca4970f6a936d5b6d5484bcb79397 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Tue, 24 Mar 2015 16:01:03 +0100
Subject: Fixing equality of notation_constrs. Fixes bug #4136.

---
 interp/notation.ml | 20 +++++++++++++++++++-
 1 file changed, 19 insertions(+), 1 deletion(-)

(limited to 'interp/notation.ml')

diff --git a/interp/notation.ml b/interp/notation.ml
index 6040c33a5e..f498761344 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -516,12 +516,30 @@ let availability_of_prim_token n printer_scope local_scopes =
 
 (* Miscellaneous *)
 
+let pair_eq f g (x1, y1) (x2, y2) = f x1 x2 && g y1 y2
+
+let ntpe_eq t1 t2 = match t1, t2 with
+| NtnTypeConstr, NtnTypeConstr -> true
+| NtnTypeConstrList, NtnTypeConstrList -> true
+| NtnTypeBinderList, NtnTypeBinderList -> true
+| (NtnTypeConstr | NtnTypeConstrList | NtnTypeBinderList), _ -> false
+
+
+let vars_eq (id1, (sc1, tp1)) (id2, (sc2, tp2)) =
+  Id.equal id1 id2 &&
+  pair_eq (Option.equal String.equal) (List.equal String.equal) sc1 sc2 &&
+  ntpe_eq tp1 tp2
+
+let interpretation_eq (vars1, t1) (vars2, t2) =
+  List.equal vars_eq vars1 vars2 &&
+  Notation_ops.eq_notation_constr t1 t2
+
 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 *)
+    interpretation_eq r' r
   with Not_found -> false
 
 let isNVar_or_NHole = function NVar _ | NHole _ -> true | _ -> false
-- 
cgit v1.2.3


From f3ff16adced3e5bf8d11cb74ee68be1267edc2b6 Mon Sep 17 00:00:00 2001
From: Guillaume Melquiond
Date: Fri, 27 Mar 2015 19:46:40 +0100
Subject: Normalize scope names before storing them in vo files. (Fix for bug
 #4162)

Note that I do not understand why the delimiter map is incomplete on
loading and thus was causing a failure. So, while the patch is the proper
way to deal with notation scopes, there might be another bug lurking in
this file.
---
 interp/notation.ml | 6 +-----
 1 file changed, 1 insertion(+), 5 deletions(-)

(limited to 'interp/notation.ml')

diff --git a/interp/notation.ml b/interp/notation.ml
index f498761344..80db2cb396 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -136,10 +136,6 @@ let scope_is_open sc = scope_is_open_in_scopes sc (!scope_stack)
 (* Exportation of scopes *)
 let open_scope i (_,(local,op,sc)) =
   if Int.equal i 1 then
-    let sc = match sc with
-      | Scope sc -> Scope (normalize_scope sc)
-      | _ -> sc
-    in
     scope_stack :=
       if op then sc :: !scope_stack
       else List.except scope_eq sc !scope_stack
@@ -166,7 +162,7 @@ let inScope : bool * bool * scope_elem -> obj =
       classify_function = classify_scope }
 
 let open_close_scope (local,opening,sc) =
-  Lib.add_anonymous_leaf (inScope (local,opening,Scope sc))
+  Lib.add_anonymous_leaf (inScope (local,opening,Scope (normalize_scope sc)))
 
 let empty_scope_stack = []
 
-- 
cgit v1.2.3