kernel/type_errors.ml

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

3 files changed, 12 insertions, 6 deletions

diff --git a/pretyping/pretype_errors.ml b/pretyping/pretype_errors.ml
index 247620a676..b8a0803668 100644
--- a/pretyping/pretype_errors.ml
+++ b/pretyping/pretype_errors.ml
@@ -49,13 +49,16 @@ let error_wrong_predicate_arity_loc loc k env c n1 n2 =
 let error_needs_inversion k env x t =
   raise (TypeError (k, env, NeedsInversion (x,t)))
 
-
 let error_ill_formed_branch_loc loc k env c i actty expty =
   raise_pretype_error (loc, k, env, IllFormedBranch (c,i,actty,expty))
 
+(*s Implicit arguments synthesis errors *)
+
+let error_unexpected_type_loc loc env actty expty =
+  raise_pretype_error (loc, CCI, env, UnexpectedType (actty, expty))
+
 let error_occur_check k env ev c =
   raise (TypeError (k, env, OccurCheck (ev,c)))
 
 let error_not_clean k env ev c =
   raise (TypeError (k, env, NotClean (ev,c)))
-
diff --git a/pretyping/pretype_errors.mli b/pretyping/pretype_errors.mli
index 8522328977..aab6abc085 100644
--- a/pretyping/pretype_errors.mli
+++ b/pretyping/pretype_errors.mli
@@ -11,7 +11,7 @@ open Type_errors
 open Rawterm
 (*i*)
 
-(* The type of errors raised by the pretyper *)
+(*s The type of errors raised by the pretyper *)
 
 val error_var_not_found_loc :
   loc -> path_kind -> identifier -> 'a
@@ -38,7 +38,7 @@ val error_number_branches_loc :
 val error_case_not_inductive_loc :
   loc -> path_kind -> env -> constr -> constr -> 'b
 
-(* Pattern-matching errors *)
+(*s Pattern-matching errors *)
 
 val error_bad_constructor_loc : 
   loc -> path_kind -> constructor -> inductive -> 'b
@@ -52,7 +52,9 @@ val error_wrong_predicate_arity_loc :
 val error_needs_inversion : path_kind -> env -> constr -> constr -> 'a
 
 
-(* Implicit arguments synthesis errors *)
+(*s Implicit arguments synthesis errors *)
+
+val error_unexpected_type_loc : loc -> env -> constr -> constr -> 'b
 
 val error_occur_check : path_kind -> env -> int -> constr -> 'a
 
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index cadaa7f78c..147960ade4 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -461,7 +461,8 @@ and pretype_type valcon env isevars lvar lmeta = function
 	then
 	  { uj_val = nf_ise1 !isevars tj.uj_val;
 	    uj_type = tj.uj_type }
-	else error "This type should be another one !"
+	else
+	  error_unexpected_type_loc (loc_of_rawconstr c) env tj.uj_val v
 
 
 let unsafe_fmachine tycon nocheck isevars metamap env lvar lmeta constr =