Add information of localisation when an error involving an "implicit

types" occurs. Also improved the "unexpected type" error message.

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

6 files changed, 13 insertions, 10 deletions

diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 096437090..fad3c4910 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -315,7 +315,7 @@ let check_capture loc ty = function
 let locate_if_isevar loc na = function
   | RHole _ ->
       (try match na with
-	| Name id ->  Reserve.find_reserved_type id
+	| Name id -> rawconstr_of_aconstr loc (Reserve.find_reserved_type id)
 	| Anonymous -> raise Not_found
       with Not_found -> RHole (loc, Evd.BinderType na))
   | x -> x
diff --git a/interp/reserve.ml b/interp/reserve.ml
index 3bcd6b1e7..2d36f2409 100644
--- a/interp/reserve.ml
+++ b/interp/reserve.ml
@@ -15,6 +15,7 @@ open Nameops
 open Summary
 open Libobject
 open Lib
+open Topconstr
 
 let reserve_table = ref Idmap.empty
 
@@ -81,7 +82,8 @@ let rec unloc = function
 let anonymize_if_reserved na t = match na with
   | Name id as na ->
       (try
-	if not !Flags.raw_print & unloc t = find_reserved_type id
+	if not !Flags.raw_print &
+	   aconstr_of_rawconstr [] [] t = find_reserved_type id
 	then RHole (dummy_loc,Evd.BinderType na)
 	else t
       with Not_found -> t)
diff --git a/interp/reserve.mli b/interp/reserve.mli
index a72aa8ec9..3bcba719c 100644
--- a/interp/reserve.mli
+++ b/interp/reserve.mli
@@ -9,7 +9,8 @@
 open Util
 open Names
 open Rawterm
+open Topconstr
 
-val declare_reserved_type : identifier located -> rawconstr -> unit
-val find_reserved_type : identifier -> rawconstr
+val declare_reserved_type : identifier located -> aconstr -> unit
+val find_reserved_type : identifier -> aconstr
 val anonymize_if_reserved : name -> rawconstr -> rawconstr
diff --git a/plugins/subtac/subtac_command.ml b/plugins/subtac/subtac_command.ml
index 7c6e54a9c..852776630 100644
--- a/plugins/subtac/subtac_command.ml
+++ b/plugins/subtac/subtac_command.ml
@@ -86,7 +86,7 @@ let interp_constr_judgment isevars env c =
 let locate_if_isevar loc na = function
   | RHole _ ->
       (try match na with
-	| Name id ->  Reserve.find_reserved_type id
+	| Name id -> rawconstr_of_aconstr loc (Reserve.find_reserved_type id)
 	| Anonymous -> raise Not_found
       with Not_found -> RHole (loc, Evd.BinderType na))
   | x -> x
diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml
index c3eb23ff6..191014c0b 100644
--- a/toplevel/himsg.ml
+++ b/toplevel/himsg.ml
@@ -201,9 +201,8 @@ let explain_cant_apply_not_functional env rator randl =
 let explain_unexpected_type env actual_type expected_type =
   let pract = pr_lconstr_env env actual_type in
   let prexp = pr_lconstr_env env expected_type in
-  str "This type is" ++ spc () ++ pract ++ spc () ++
-  str "but is expected to be" ++
-  spc () ++ prexp ++ str "."
+  str "Found type" ++ spc () ++ pract ++ spc () ++
+  str "where" ++ spc () ++ prexp ++ str " was expected."
 
 let explain_not_product env c =
   let pr = pr_lconstr_env env c in
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index ee69f5574..fe676b3b1 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -797,8 +797,9 @@ let vernac_declare_implicits local r = function
 let vernac_reserve bl =
   let sb_decl = (fun (idl,c) ->
     let t = Constrintern.interp_type Evd.empty (Global.env()) c in
-      let t = Detyping.detype false [] [] t in
-        List.iter (fun id -> Reserve.declare_reserved_type id t) idl)
+    let t = Detyping.detype false [] [] t in
+    let t = aconstr_of_rawconstr [] [] t in
+    List.iter (fun id -> Reserve.declare_reserved_type id t) idl)
   in List.iter sb_decl bl
 
 let vernac_generalizable = Implicit_quantifiers.declare_generalizable