Messages d'erreur Cases

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1703 85f007b7-540e-0410-9357-904b9bb8a0f7

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