GROS COMMIT:

 - reduction du noyau (variables existentielles, fonctions auxiliaires
   pour inventer des noms, etc. deplacees hors de kernel/)
 - changement de noms de constructeurs des constr (suppression de "Is" et
   "Mut")


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

1 files changed, 32 insertions, 27 deletions

diff --git a/pretyping/pretype_errors.ml b/pretyping/pretype_errors.ml
index 2d52ad5fde..fd42ca0ba9 100644
--- a/pretyping/pretype_errors.ml
+++ b/pretyping/pretype_errors.ml
@@ -12,10 +12,11 @@ open Util
 open Names
 open Sign
 open Term
+open Termops
 open Environ
 open Type_errors
 open Rawterm
-open Inductive
+open Inductiveops
 
 type ml_case_error =
   | MlCaseAbsurd
@@ -35,14 +36,7 @@ type pretype_error =
 
 exception PretypeError of env * pretype_error
 
-(* Replacing defined evars for error messages *)
-let rec whd_evar sigma c =
-  match kind_of_term c with
-    | IsEvar (ev,args) when Evd.in_dom sigma ev & Evd.is_defined sigma ev ->
-	whd_evar sigma (Instantiate.existential_value sigma (ev,args))
-    | _ -> collapse_appl c
-
-let nf_evar sigma = Reduction.local_strong (whd_evar sigma)
+let nf_evar = Reductionops.nf_evar
 let j_nf_evar sigma j = 
   { uj_val = nf_evar sigma j.uj_val;
     uj_type = nf_evar sigma j.uj_type }
@@ -52,13 +46,22 @@ let tj_nf_evar sigma {utj_val=v;utj_type=t} =
   {utj_val=type_app (nf_evar sigma) v;utj_type=t}
 
 let env_ise sigma env =
-  map_context (nf_evar sigma) env
+  let sign = named_context env in
+  let ctxt = rel_context env in
+  let env0 = reset_with_named_context sign env in
+  Sign.fold_rel_context
+    (fun (na,b,ty) e ->
+      push_rel
+        (na, option_app (nf_evar sigma) b, nf_evar sigma ty)
+        e)
+    ctxt
+    env0
 
 (* This simplify the typing context of Cases clauses *)
 (* hope it does not disturb other typing contexts *)
 let contract env lc =
   let l = ref [] in
-  let contract_context env (na,c,t) =
+  let contract_context (na,c,t) env =
     match c with
       | Some c' when isRel c' ->
 	  l := (substl !l c') :: !l;
@@ -81,50 +84,52 @@ let contract3 env a b c = match contract env [a;b;c] with
 let raise_pretype_error (loc,ctx,sigma,te) =
   Stdpp.raise_with_loc loc (PretypeError(env_ise sigma ctx,te))
 
-let raise_located_type_error (loc,k,ctx,sigma,te) =
-  Stdpp.raise_with_loc loc (TypeError(k,env_ise sigma ctx,te))
+let raise_located_type_error (loc,ctx,sigma,te) =
+  Stdpp.raise_with_loc loc (TypeError(env_ise sigma ctx,te))
 
 
 let error_actual_type_loc loc env sigma {uj_val=c;uj_type=actty} expty =
   let env, c, actty, expty = contract3 env c actty expty in
+  let j = j_nf_evar sigma {uj_val=c;uj_type=actty} in
   raise_located_type_error
-    (loc, CCI, env, sigma,
-     ActualType (c,nf_evar sigma actty, nf_evar sigma expty))
+    (loc, env, sigma, ActualType (j, nf_evar sigma expty))
 
 let error_cant_apply_not_functional_loc loc env sigma rator randl =
+  let ja = Array.of_list (jl_nf_evar sigma randl) in
   raise_located_type_error
-    (loc, CCI, env, sigma,
-    CantApplyNonFunctional (j_nf_evar sigma rator, jl_nf_evar sigma randl))
+    (loc, env, sigma,
+    CantApplyNonFunctional (j_nf_evar sigma rator, ja))
 
 let error_cant_apply_bad_type_loc loc env sigma (n,c,t) rator randl =
+  let ja = Array.of_list (jl_nf_evar sigma randl) in
   raise_located_type_error
-    (loc, CCI, env, sigma,
+    (loc, env, sigma,
      CantApplyBadType
        ((n,nf_evar sigma c, nf_evar sigma t),
-        j_nf_evar sigma rator, jl_nf_evar sigma randl))
+        j_nf_evar sigma rator, ja))
 
 let error_cant_find_case_type_loc loc env sigma expr =
   raise_pretype_error
     (loc, env, sigma, CantFindCaseType (nf_evar sigma expr))
 
-let error_ill_formed_branch_loc loc k env sigma c i actty expty =
+let error_ill_formed_branch_loc loc env sigma c i actty expty =
   let simp t = Reduction.nf_betaiota (nf_evar sigma t) in
   raise_located_type_error
-    (loc, k, env, sigma,
+    (loc, env, sigma,
      IllFormedBranch (nf_evar sigma c,i,simp actty, simp expty))
 
-let error_number_branches_loc loc k env sigma cj expn =
+let error_number_branches_loc loc env sigma cj expn =
   raise_located_type_error
-    (loc, k, env, sigma,
+    (loc, env, sigma,
      NumberBranches (j_nf_evar sigma cj, expn))
 
-let error_case_not_inductive_loc loc k env sigma cj =
+let error_case_not_inductive_loc loc env sigma cj =
   raise_located_type_error
-    (loc, k, env, sigma, CaseNotInductive (j_nf_evar sigma cj))
+    (loc, env, sigma, CaseNotInductive (j_nf_evar sigma cj))
 
-let error_ill_typed_rec_body_loc loc k env sigma i na jl tys =
+let error_ill_typed_rec_body_loc loc env sigma i na jl tys =
   raise_located_type_error
-    (loc, k, env, sigma,
+    (loc, env, sigma,
      IllTypedRecBody (i,na,jv_nf_evar sigma jl,
                       Array.map (nf_evar sigma) tys))