diff options
Diffstat (limited to 'interp')
| -rw-r--r-- | interp/constrintern.ml | 2 | ||||
| -rw-r--r-- | interp/notation.ml | 3 |
2 files changed, 3 insertions, 2 deletions
diff --git a/interp/constrintern.ml b/interp/constrintern.ml index 51c8e2e10a..74a49152ca 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -833,7 +833,7 @@ let check_number_of_pattern loc n l = if not (Int.equal n p) then raise (InternalizationError (loc,BadPatternsNumber (n,p))) let check_or_pat_variables loc ids idsl = - if List.exists (fun ids' -> not (List.eq_set ids ids')) idsl then + if List.exists (fun ids' -> not (List.eq_set Id.equal ids ids')) idsl then user_err_loc (loc, "", str "The components of this disjunctive pattern must bind the same variables.") 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 |