diff options
Diffstat (limited to 'interp/notation.ml')
| -rw-r--r-- | interp/notation.ml | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/interp/notation.ml b/interp/notation.ml index 2363789fab..b661c33c6b 100644 --- a/interp/notation.ml +++ b/interp/notation.ml @@ -135,7 +135,8 @@ let open_scope i (_,(local,op,sc)) = | _ -> sc in scope_stack := - if op then sc :: !scope_stack else List.except sc !scope_stack + if op then sc :: !scope_stack + else List.except Pervasives.(=) sc !scope_stack (* FIXME *) let cache_scope o = open_scope 1 o |