diff options
-rw-r--r-- | parsing/astterm.ml | 9 | ||||
-rw-r--r-- | toplevel/himsg.ml | 8 |
2 files changed, 10 insertions, 7 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 diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml index 34cb1a13b..9ce8aad99 100644 --- a/toplevel/himsg.ml +++ b/toplevel/himsg.ml @@ -478,11 +478,11 @@ let explain_bad_pattern ctx cstr ty = let explain_bad_constructor ctx cstr ind = let pi = pr_inductive ctx ind in - let pc = pr_constructor ctx cstr in +(* let pc = pr_constructor ctx cstr in*) let pt = pr_inductive ctx (inductive_of_constructor cstr) in - [< 'sTR "Expecting a constructor in inductive type "; pi; 'bRK(1,1) ; - 'sTR " but found the constructor " ; pc; 'bRK(1,1) ; - 'sTR " in inductive type "; pt >] + [< 'sTR "Found a constructor of inductive type "; pt; 'bRK(1,1) ; + 'sTR "while a constructor of " ; pi; 'bRK(1,1) ; + 'sTR "is expected" >] let explain_wrong_numarg_of_constructor ctx cstr n = let pc = pr_constructor ctx (cstr,[||]) in |