From 47d4276763971f155c81f4e299d855883b6c9408 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Sat, 2 Jun 2018 22:10:15 +0200 Subject: Fixes #7641: more detailed message for disjunctive patterns with different vars. Could still be made more detailed with more time. --- interp/constrintern.ml | 15 ++++++++++++--- 1 file changed, 12 insertions(+), 3 deletions(-) (limited to 'interp') diff --git a/interp/constrintern.ml b/interp/constrintern.ml index 45c0e9c42..f77c4d327 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -1141,9 +1141,18 @@ 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 (fun {loc;v=id} {v=id'} -> Id.equal id id') ids ids')) idsl then - user_err ?loc (str - "The components of this disjunctive pattern must bind the same variables.") + let eq_id {v=id} {v=id'} = Id.equal id id' in + (* Collect remaining patterns which do not have the same variables as the first pattern *) + let idsl = List.filter (fun ids' -> not (List.eq_set eq_id ids ids')) idsl in + match idsl with + | ids'::_ -> + (* Look for an [id] which is either in [ids] and not in [ids'] or in [ids'] and not in [ids] *) + let ids'' = List.subtract eq_id ids ids' in + let ids'' = if ids'' = [] then List.subtract eq_id ids' ids else ids'' in + user_err ?loc + (strbrk "The components of this disjunctive pattern must bind the same variables (" ++ + Id.print (List.hd ids'').v ++ strbrk " is not bound in all patterns).") + | [] -> () (** Use only when params were NOT asked to the user. @return if letin are included *) -- cgit v1.2.3