Localisation des erreurs de sorte du prétypage

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

5 files changed, 16 insertions, 9 deletions

diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml
index 51fea11a2..d2c3e255c 100644
--- a/pretyping/coercion.ml
+++ b/pretyping/coercion.ml
@@ -89,15 +89,16 @@ let inh_app_fun env isevars j =
            (isevars,apply_coercion env p j t)
 	 with Not_found -> (isevars,j))
 
-let inh_tosort_force env isevars j =
+let inh_tosort_force loc env isevars j =
   try
     let t,i1 = class_of1 env (evars_of isevars) j.uj_type in
     let p = lookup_path_to_sort_from i1 in
-    apply_coercion env p j t 
-  with Not_found -> 
-    j
+    let j1 = apply_coercion env p j t in 
+    (isevars,type_judgment env (j_nf_evar (evars_of isevars) j1))
+  with Not_found ->
+    error_not_a_type_loc loc env (evars_of isevars) j
 
-let inh_coerce_to_sort env isevars j =
+let inh_coerce_to_sort loc env isevars j =
   let typ = whd_betadeltaiota env (evars_of isevars) j.uj_type in
   match kind_of_term typ with
     | Sort s -> (isevars,{ utj_val = j.uj_val; utj_type = s })
@@ -105,8 +106,7 @@ let inh_coerce_to_sort env isevars j =
 	let (isevars',s) = define_evar_as_sort isevars ev in
 	(isevars',{ utj_val = j.uj_val; utj_type = s })
     | _ ->
-        let j1 = inh_tosort_force env isevars j in 
-	(isevars,type_judgment env (j_nf_evar (evars_of isevars) j1))
+	inh_tosort_force loc env isevars j
 
 let inh_coerce_to_fail env isevars c1 hj =
   let hj' =
diff --git a/pretyping/coercion.mli b/pretyping/coercion.mli
index c3b470307..f5356d432 100644
--- a/pretyping/coercion.mli
+++ b/pretyping/coercion.mli
@@ -30,7 +30,7 @@ val inh_app_fun :
 (* [inh_coerce_to_sort env isevars j] coerces [j] to a type; i.e. it
    inserts a coercion into [j], if needed, in such a way it gets as
    type a sort; it fails if no coercion is applicable *)
-val inh_coerce_to_sort :
+val inh_coerce_to_sort : loc ->
   env -> evar_defs -> unsafe_judgment -> evar_defs * unsafe_type_judgment
 
 (* [inh_conv_coerce_to loc env isevars j t] coerces [j] to an object of type 
diff --git a/pretyping/pretype_errors.ml b/pretyping/pretype_errors.ml
index f1f95695d..d87a26c22 100644
--- a/pretyping/pretype_errors.ml
+++ b/pretyping/pretype_errors.ml
@@ -136,6 +136,9 @@ let error_ill_typed_rec_body_loc loc env sigma i na jl tys =
      IllTypedRecBody (i,na,jv_nf_evar sigma jl,
                       Array.map (nf_evar sigma) tys))
 
+let error_not_a_type_loc loc env sigma j =
+  raise_located_type_error (loc, env, sigma, NotAType (j_nf_evar sigma j))
+
 (*s Implicit arguments synthesis errors. It is hard to find
     a precise location. *)
 
diff --git a/pretyping/pretype_errors.mli b/pretyping/pretype_errors.mli
index ee4cdb206..dc8fdd03d 100644
--- a/pretyping/pretype_errors.mli
+++ b/pretyping/pretype_errors.mli
@@ -79,6 +79,9 @@ val error_ill_typed_rec_body_loc :
   loc -> env ->  Evd.evar_map ->
       int -> name array -> unsafe_judgment array -> types array -> 'b
 
+val error_not_a_type_loc :
+  loc -> env -> Evd.evar_map -> unsafe_judgment -> 'b
+
 (*s Implicit arguments synthesis errors *)
 
 val error_occur_check : env ->  Evd.evar_map -> existential_key -> constr -> 'b
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 3e0ac7471..8a91cf61e 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -467,7 +467,8 @@ and pretype_type valcon env isevars lvar = function
 	       utj_type = s})
   | c ->
       let j = pretype empty_tycon env isevars lvar c in
-      let tj = evd_comb1 (inh_coerce_to_sort env) isevars j in
+      let loc = loc_of_rawconstr c in
+      let tj = evd_comb1 (inh_coerce_to_sort loc env) isevars j in
       match valcon with
 	| None -> tj
 	| Some v ->