Modification messages d'erreurs, possibilité de n'importe quel constr dans les instances de références

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

5 files changed, 21 insertions, 17 deletions

diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml
index 15577dd9e7..c98eeab160 100644
--- a/pretyping/coercion.ml
+++ b/pretyping/coercion.ml
@@ -167,7 +167,7 @@ let inh_cast_rel env isevars cj tj =
     uj_kind = whd_betadeltaiota env !isevars tj.uj_type }
 
 let inh_apply_rel_list nocheck env isevars argjl funj vtcon =
-  let rec apply_rec acc typ = function
+  let rec apply_rec n acc typ = function
     | [] -> 
 	let resj =
       	  { uj_val=applist(j_val_only funj,List.map j_val_only (List.rev acc));
@@ -190,14 +190,14 @@ let inh_apply_rel_list nocheck env isevars argjl funj vtcon =
 		  (try 
 		     inh_conv_coerce_to env isevars c1 hj 
 		   with Failure _ | Not_found ->
-                     error_cant_apply CCI env "Type Error" 
-		       (j_nf_ise env !isevars funj) 
+                     error_cant_apply_bad_type CCI env (n,c1,hj.uj_type)
+		       (j_nf_ise env !isevars funj)
 		       (jl_nf_ise env !isevars argjl)) 
 	      in
-              apply_rec (hj'::acc) (subst1 hj'.uj_val c2) restjl
+              apply_rec (n+1) (hj'::acc) (subst1 hj'.uj_val c2) restjl
           | _ ->
-              error_cant_apply CCI env "Non-functional construction" 
+              error_cant_apply_not_functional CCI env
 	      	(j_nf_ise env !isevars funj) (jl_nf_ise env !isevars argjl)
   in 
-  apply_rec [] funj.uj_type argjl
+  apply_rec 1 [] funj.uj_type argjl
 
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index 34ffa2f950..901e60b8c8 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -314,13 +314,15 @@ let rec detype avoid env t =
     | IsAppL (f,args) ->
 	RApp (dummy_loc,detype avoid env f,List.map (detype avoid env) args)
     | IsConst (sp,cl) ->
-	RRef(dummy_loc,RConst(sp,cl))
+	RRef(dummy_loc,RConst(sp,Array.map (detype avoid env) cl))
     | IsEvar (ev,cl) ->
-	RRef(dummy_loc,REVar(ev,cl))
+	RRef(dummy_loc,REVar(ev,Array.map (detype avoid env) cl))
     | IsAbst (sp,cl) -> 
 	anomaly "bdize: Abst should no longer occur in constr"
-    | IsMutInd (ind_sp,cl) -> RRef (dummy_loc,RInd (ind_sp,cl))
-    | IsMutConstruct (cstr_sp,cl) -> RRef (dummy_loc,RConstruct (cstr_sp,cl))
+    | IsMutInd (ind_sp,cl) ->
+	RRef (dummy_loc,RInd (ind_sp,Array.map (detype avoid env) cl))
+    | IsMutConstruct (cstr_sp,cl) ->
+	RRef (dummy_loc,RConstruct (cstr_sp,Array.map (detype avoid env) cl))
     | IsMutCase (annot,p,c,bl) ->
 	let synth_type = synthetize_type () in
 	let tomatch = detype avoid env c in
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 2f059f6c10..5d64f6e230 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -212,11 +212,11 @@ let pretype_var loc env lvar id =
 let trad_metamap = ref []
 let trad_nocheck = ref false
 
-let pretype_ref loc isevars env lvar = function
+let pretype_ref pretype loc isevars env lvar = function
 | RVar id -> pretype_var loc env lvar id
 
 | RConst (sp,ctxt) ->
-    let cst = (sp,ctxt_of_ids ctxt) in
+    let cst = (sp,Array.map pretype ctxt) in
     make_judge (mkConst cst) (type_of_constant env !isevars cst)
 
 | RAbst sp -> failwith "Pretype: abst doit disparaître"
@@ -246,11 +246,11 @@ let pretype_ref loc isevars env lvar = function
     make_judge cstr (type_of_existential env !isevars cstr)
 *)
 | RInd (ind_sp,ctxt) ->
-    let ind = (ind_sp,ctxt_of_ids ctxt) in
+    let ind = (ind_sp,Array.map pretype ctxt) in
     make_judge (mkMutInd ind) (type_of_inductive env !isevars ind)
  
 | RConstruct (cstr_sp,ctxt) ->
-    let cstr = (cstr_sp,ctxt_of_ids ctxt) in
+    let cstr = (cstr_sp,Array.map pretype ctxt) in
     let (typ,kind) = destCast (type_of_constructor env !isevars cstr) in
     {uj_val=mkMutConstruct cstr; uj_type=typ; uj_kind=kind}
 
@@ -266,7 +266,9 @@ let rec pretype vtcon env isevars lvar lmeta cstr =
 match cstr with   (* Où teste-t-on que le résultat doit satisfaire tycon ? *)
 
 | RRef (loc,ref) -> 
-    pretype_ref loc isevars env lvar ref
+    pretype_ref
+      (fun c -> (pretype empty_tycon env isevars lvar lmeta c).uj_val)
+      loc isevars env lvar ref
 
 | RMeta (loc,n) ->
     (try
diff --git a/pretyping/rawterm.ml b/pretyping/rawterm.ml
index 78b87426fd..a3382f5cdf 100644
--- a/pretyping/rawterm.ml
+++ b/pretyping/rawterm.ml
@@ -23,7 +23,7 @@ type rawsort = RProp of Term.contents | RType
 
 (*i Pas beau ce constr dans rawconstr, mais mal compris ce ctxt des ref i*)
 type rawconstr = 
-  | RRef of loc * constr array reference
+  | RRef of loc * rawconstr array reference
   | RMeta of loc * int
   | RApp of loc * rawconstr * rawconstr list
   | RBinder of loc * binder_kind * name * rawconstr * rawconstr
diff --git a/pretyping/rawterm.mli b/pretyping/rawterm.mli
index 1cff2989f5..5fb28fea03 100644
--- a/pretyping/rawterm.mli
+++ b/pretyping/rawterm.mli
@@ -21,7 +21,7 @@ type cases_pattern =
 type rawsort = RProp of Term.contents | RType
 
 type rawconstr = 
-  | RRef of loc * constr array reference
+  | RRef of loc * rawconstr array reference
   | RMeta of loc * int
   | RApp of loc * rawconstr * rawconstr list
   | RBinder of loc * binder_kind * name * rawconstr * rawconstr