From 5e6145c871eea1e94566b252b4bfc4cd752f42d5 Mon Sep 17 00:00:00 2001 From: letouzey Date: Wed, 23 Oct 2013 22:17:07 +0000 Subject: cList: set-as-list functions are now with an explicit comparison git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16920 85f007b7-540e-0410-9357-904b9bb8a0f7 --- interp/notation.ml | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) (limited to 'interp/notation.ml') 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 -- cgit v1.2.3