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(-)

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