diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2014-03-01 18:26:26 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2014-03-01 22:45:39 +0100 |
| commit | 87b510e5b0f363724eae5db9f177f167a3586015 (patch) | |
| tree | 204c7ad1e1ba38945ab58d74e28d8cf67201fe71 /interp/notation.ml | |
| parent | bca756eaebf16b6145c65b53629219d2a0a8b1ba (diff) | |
Fixing pervasive comparisons
Diffstat (limited to 'interp/notation.ml')
| -rw-r--r-- | interp/notation.ml | 8 |
1 files changed, 7 insertions, 1 deletions
diff --git a/interp/notation.ml b/interp/notation.ml index a9206b933..867e23395 100644 --- a/interp/notation.ml +++ b/interp/notation.ml @@ -116,6 +116,12 @@ let normalize_scope sc = type scope_elem = Scope of scope_name | SingleNotation of string type scopes = scope_elem list +let scope_eq s1 s2 = match s1, s2 with +| Scope s1, Scope s2 +| SingleNotation s1, SingleNotation s2 -> String.equal s1 s2 +| Scope _, SingleNotation _ +| SingleNotation _, Scope _ -> false + let scope_stack = ref [] let current_scopes () = !scope_stack @@ -136,7 +142,7 @@ let open_scope i (_,(local,op,sc)) = in scope_stack := if op then sc :: !scope_stack - else List.except Pervasives.(=) sc !scope_stack (* FIXME *) + else List.except scope_eq sc !scope_stack let cache_scope o = open_scope 1 o |