diff options
| author |  Guillaume Melquiond <guillaume.melquiond@inria.fr> | 2015-03-27 19:46:40 +0100 |
|---|---|---|
| committer | Guillaume Melquiond <guillaume.melquiond@inria.fr> | 2015-03-27 19:46:49 +0100 |
| commit | f3ff16adced3e5bf8d11cb74ee68be1267edc2b6 (patch) | |
| tree | 8c6d9cfeedd2dc391b03c77a09c60a276f17a0a7 /interp/notation.ml | |
| parent | e8b4756c655eacd8a2b9b23630ba02dbbbc4e96e (diff) | |
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.
Diffstat (limited to 'interp/notation.ml')
| -rw-r--r-- | interp/notation.ml | 6 |
1 files changed, 1 insertions, 5 deletions
diff --git a/interp/notation.ml b/interp/notation.ml index f49876134..80db2cb39 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 = [] |