diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2001-04-24 20:05:19 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2001-04-24 20:05:19 +0000 |
| commit | bd77a6421a3d398d8f7a9c9e21fb078eca20cef8 (patch) | |
| tree | f91d0e49c000d5ed0ce8a088af0cb32514084b00 /parsing | |
| parent | 9e19a6257e14619eed8e60987a445c3afa57557b (diff) | |
Messages d'erreur Cases
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1703 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'parsing')
| -rw-r--r-- | parsing/astterm.ml | 9 |
1 files changed, 6 insertions, 3 deletions
diff --git a/parsing/astterm.ml b/parsing/astterm.ml index 6a527d43e..8321d4478 100644 --- a/parsing/astterm.ml +++ b/parsing/astterm.ml @@ -67,9 +67,12 @@ let rec has_duplicate = function | [] -> None | x::l -> if List.mem x l then (Some x) else has_duplicate l -let check_linearity loc ids = +let loc_of_lhs lhs = join_loc (loc (List.hd lhs)) (loc (list_last lhs)) + +let check_linearity lhs ids = match has_duplicate ids with - | Some id -> user_err_loc (loc,"ast_to_eqn",non_linearl_mssg id) + | Some id -> + user_err_loc (loc_of_lhs lhs,"ast_to_eqn",non_linearl_mssg id) | None -> () let mal_formed_mssg () = @@ -511,7 +514,7 @@ let ast_to_rawconstr sigma env allow_soapp lvar = let eqn_ids = List.flatten idsl in let subst = List.flatten substl in (* Linearity implies the order in ids is irrelevant *) - check_linearity loc eqn_ids; + check_linearity lhs eqn_ids; check_uppercase loc eqn_ids; check_number_of_pattern loc n pl; let rhs = replace_vars_ast subst rhs in |