amelioration des messages d'erreurs vis a vis des evars

ajout automatique des chemins vers les sources au moment du Drop


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

12 files changed, 266 insertions, 174 deletions

diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index b207f4247..f69ca6084 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -102,7 +102,7 @@ let branch_scheme env isevars isrec (IndFamily (mis,params) as indf) =
 (* B) Building ML like case expressions without types *)
 
 let concl_n env sigma = 
-  let rec decrec m c = if m = 0 then c else 
+  let rec decrec m c = if m = 0 then (nf_evar sigma c) else 
     match kind_of_term (whd_betadeltaiota env sigma c) with
       | IsProd (n,_,c_0) -> decrec (m-1) c_0
       | _                -> failwith "Typing.concl_n"
@@ -151,12 +151,15 @@ let pred_case_ml_fail env sigma isrec (IndType (indf,realargs)) (i,ft) =
 
 let pred_case_ml loc env sigma isrec indt lf (i,ft) = 
   try pred_case_ml_fail env sigma isrec indt (i,ft)
-  with NotInferable e -> error_ml_case_loc loc env e indt lf.(i-1) ft
+  with NotInferable e ->
+    let j = {uj_val=lf.(i-1); uj_type=ft} in
+    error_ml_case_loc loc env sigma e indt j
 
 (* similar to pred_case_ml but does not expect the list lf of braches *)
-let pred_case_ml_onebranch loc env sigma isrec indt (i,f,ft) = 
-  try pred_case_ml_fail env sigma isrec indt (i,ft)
-  with NotInferable e -> error_ml_case_loc loc env e indt f ft
+let pred_case_ml_onebranch loc env sigma isrec indt (i,fj) = 
+  try pred_case_ml_fail env sigma isrec indt (i,fj.uj_type)
+  with NotInferable e ->
+    error_ml_case_loc loc env sigma e indt fj
 
 (************************************************************************)
 (*            Pattern-matching compilation (Cases)                      *)
@@ -1316,7 +1319,7 @@ let coerce_row typing_fun isevars env cstropt tomatch =
 		 (constructor_of_rawconstructor c) mind
 	     with Induc ->
 	       error_case_not_inductive_loc
-		 (loc_of_rawconstr tomatch) CCI env j.uj_val typ)
+		 (loc_of_rawconstr tomatch) CCI env (evars_of isevars) j)
       | None -> 
 	  try IsInd (typ,find_rectype env (evars_of isevars) typ)
 	  with Induc -> NotInd typ
diff --git a/pretyping/cases.mli b/pretyping/cases.mli
index a7dddb5cb..7e5fda903 100644
--- a/pretyping/cases.mli
+++ b/pretyping/cases.mli
@@ -35,7 +35,7 @@ val branch_scheme :
   env -> 'a evar_defs -> bool -> inductive_family -> constr array
 
 val pred_case_ml_onebranch : loc -> env -> 'c evar_map -> bool ->
-  inductive_type -> int * constr * constr -> constr 
+  inductive_type -> int * unsafe_judgment -> constr 
 
 (* Compilation of pattern-matching. *)
 
diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml
index 3e5e064bc..3cad7122c 100644
--- a/pretyping/coercion.ml
+++ b/pretyping/coercion.ml
@@ -22,13 +22,7 @@ open Retyping
 
 (* Typing operations dealing with coercions *)
 
-let class_of1 env sigma t = class_of env sigma (nf_ise1 sigma t)
-
-let j_nf_ise env sigma {uj_val=v;uj_type=t} =
-  { uj_val = nf_ise1 sigma v; 
-    uj_type = nf_ise1 sigma t }
-
-let jl_nf_ise env sigma = List.map (j_nf_ise env sigma)
+let class_of1 env sigma t = class_of env sigma (nf_evar sigma t)
 
 (* Here, funj is a coercion therefore already typed in global context *)
 let apply_coercion_args env argl funj =
@@ -150,10 +144,9 @@ let inh_conv_coerce_to loc env isevars cj t =
   let cj' = 
     try 
       inh_conv_coerce_to_fail env isevars t cj 
-    with NoCoercion -> 
-      let rcj = j_nf_ise env (evars_of isevars) cj in
-      let at = nf_ise1 (evars_of isevars) t in
-      error_actual_type_loc loc env rcj.uj_val rcj.uj_type at
+    with NoCoercion ->
+      let sigma = evars_of isevars in
+      error_actual_type_loc loc env sigma cj t
   in
   { uj_val = cj'.uj_val; uj_type = t }
 
@@ -165,40 +158,25 @@ let inh_apply_rel_list apploc env isevars argjl (funloc,funj) tycon =
   let rec apply_rec env n resj = function
     | [] -> resj
     | (loc,hj)::restjl ->
+        let sigma = evars_of isevars in
 	let resj = inh_app_fun env isevars resj in
-        let ntyp = whd_betadeltaiota env (evars_of isevars) resj.uj_type in
+        let ntyp = whd_betadeltaiota env sigma resj.uj_type in
       	match kind_of_term ntyp with
           | IsProd (na,c1,c2) ->
               let hj' =
 		try 
 		  inh_conv_coerce_to_fail env isevars c1 hj 
 		with NoCoercion ->
-(*
-                  error_cant_apply_bad_type_loc apploc env 
-		    (n,nf_ise1 (evars_of isevars) c1,
-		     nf_ise1 (evars_of isevars) hj.uj_type)
-		    (j_nf_ise env (evars_of isevars) funj)
-		    (jl_nf_ise env (evars_of isevars) argjl) in
-*)
-                  error_cant_apply_bad_type_loc apploc env 
-		    (1,nf_ise1 (evars_of isevars) c1,
-		     nf_ise1 (evars_of isevars) hj.uj_type)
-		    (j_nf_ise env (evars_of isevars) resj)
-		    (jl_nf_ise env (evars_of isevars) (List.map snd restjl)) in
+                  error_cant_apply_bad_type_loc apploc env sigma
+		    (1,c1,hj.uj_type) resj (List.map snd restjl) in
 	      let newresj =
       		{ uj_val = applist (j_val resj, [j_val hj']);
 		  uj_type = subst1 hj'.uj_val c2 } in
 	      apply_rec (push_rel_assum (na,c1) env) (n+1) newresj restjl
           | _ ->
-(*
-              error_cant_apply_not_functional_loc apploc env
-	      	(j_nf_ise env (evars_of isevars) funj)
-                (jl_nf_ise env (evars_of isevars) argjl)
-*)
               error_cant_apply_not_functional_loc 
-		(Rawterm.join_loc funloc loc) env
-	      	(j_nf_ise env (evars_of isevars) resj)
-		(jl_nf_ise env (evars_of isevars) (List.map snd restjl))
+		(Rawterm.join_loc funloc loc) env sigma resj
+                (List.map snd restjl)
   in 
   apply_rec env 1 funj argjl
 
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index 766e6e0e9..6783e70a4 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -52,8 +52,9 @@ let evar_apprec env isevars stack c =
  * possibly applied to arguments. *)
 
 let rec evar_conv_x env isevars pbty term1 term2 = 
-  let term1 = whd_ise1 (evars_of isevars) term1 in
-  let term2 = whd_ise1 (evars_of isevars) term2 in
+  let sigma = evars_of isevars in
+  let term1 = whd_castappevar sigma term1 in
+  let term2 = whd_castappevar sigma term2 in
 (*
  if eq_constr term1 term2 then 
     true
@@ -63,7 +64,7 @@ let rec evar_conv_x env isevars pbty term1 term2 =
     is_fconv pbty env (evars_of isevars) term1 term2
   else
 *)
-  (is_fconv pbty env (evars_of isevars) term1 term2) or
+  (is_fconv pbty env sigma term1 term2) or
   if ise_undefined isevars term1 then
     solve_simple_eqn evar_conv_x env isevars (pbty,destEvar term1,term2)
   else if ise_undefined isevars term2 then
@@ -206,15 +207,15 @@ and evar_eqappr_x env isevars pbty (term1,l1 as appr1) (term2,l2 as appr2) =
 	| IsLambda (na,c1,c'1), IsLambda (_,c2,c'2) when l1=[] & l2=[] -> 
 	    evar_conv_x env isevars CONV c1 c2
 	    & 
-	    (let c = nf_ise1 (evars_of isevars) c1 in
+	    (let c = nf_evar (evars_of isevars) c1 in
              evar_conv_x (push_rel_assum (na,c) env) isevars CONV c'1 c'2)
 
 	| IsLetIn (na,b1,t1,c'1), IsLetIn (_,b2,_,c'2) ->
 	    let f1 () =
 	      evar_conv_x env isevars CONV b1 b2
 	      & 
-              (let b = nf_ise1 (evars_of isevars) b1 in
-	       let t = nf_ise1 (evars_of isevars) t1 in
+              (let b = nf_evar (evars_of isevars) b1 in
+	       let t = nf_evar (evars_of isevars) t1 in
                evar_conv_x (push_rel_def (na,b,t) env) isevars pbty c'1 c'2)
 	      & (List.length l1 = List.length l2)
 	      & (List.for_all2 (evar_conv_x env isevars CONV) l1 l2)
@@ -236,7 +237,7 @@ and evar_eqappr_x env isevars pbty (term1,l1 as appr1) (term2,l2 as appr2) =
 	| IsProd (n,c1,c'1), IsProd (_,c2,c'2) when l1=[] & l2=[] -> 
             evar_conv_x env isevars CONV c1 c2
             & 
-	    (let c = nf_ise1 (evars_of isevars) c1 in
+	    (let c = nf_evar (evars_of isevars) c1 in
 	     evar_conv_x (push_rel_assum (n,c) env) isevars pbty c'1 c'2)
 
 	| IsMutInd (sp1,cl1), IsMutInd (sp2,cl2) ->
diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml
index f10973afb..5b4a0dccb 100644
--- a/pretyping/evarutil.ml
+++ b/pretyping/evarutil.ml
@@ -47,6 +47,44 @@ let filter_sign p sign x =
     (x,[],nil_sign)
 *)
 
+(* Expanding existential variables (pretyping.ml) *)
+(* 1- whd_ise fails if an existential is undefined *)
+
+exception Uninstantiated_evar of int
+
+let rec whd_ise sigma c =
+  match kind_of_term c with
+    | IsEvar (ev,args) when Evd.in_dom sigma ev ->
+	if Evd.is_defined sigma ev then
+          whd_ise sigma (existential_value sigma (ev,args))
+	else raise (Uninstantiated_evar ev)
+  | _ -> c
+
+
+(* Expand evars, possibly in the head of an application *)
+let whd_castappevar_stack sigma c = 
+  let rec whrec (c, l as s) =
+    match kind_of_term c with
+      | IsEvar (ev,args) when Evd.in_dom sigma ev & Evd.is_defined sigma ev -> 
+	  whrec (existential_value sigma (ev,args), l)
+      | IsCast (c,_) -> whrec (c, l)
+      | IsApp (f,args) -> whrec (f, Array.fold_right (fun a l -> a::l) args l)
+      | _ -> s
+  in 
+  whrec (c, [])
+
+let whd_castappevar sigma c = applist (whd_castappevar_stack sigma c)
+
+let nf_evar = Pretype_errors.nf_evar
+let j_nf_evar = Pretype_errors.j_nf_evar
+let jl_nf_evar = Pretype_errors.jl_nf_evar
+let jv_nf_evar = Pretype_errors.jv_nf_evar
+let tj_nf_evar = Pretype_errors.tj_nf_evar
+
+(**********************)
+(* Creating new evars *)
+(**********************)
+
 let evar_env evd = Global.env_of_context evd.evar_hyps
 
 (* Generator of existential names *)
@@ -200,7 +238,7 @@ let need_restriction isevars args = not (array_for_all closed0 args)
  * false. The problem is that we won't get the right error message.
  *)
 
-let real_clean isevars sp args rhs =
+let real_clean isevars ev args rhs =
   let subst = List.map (fun (x,y) -> (y,mkVar x)) (filter_unique args) in
   let rec subs k t =
     match kind_of_term t with
@@ -224,7 +262,8 @@ let real_clean isevars sp args rhs =
       | _ -> map_constr_with_binders succ subs k t
   in
   let body = subs 0 rhs in
-  if not (closed0 body) then error_not_clean empty_env sp body;
+  if not (closed0 body)
+  then error_not_clean empty_env isevars.evars ev body;
   body
 
 let make_evar_instance_with_rel env =
@@ -280,7 +319,8 @@ let keep_rels_and_vars c = match kind_of_term c with
   | _ -> mkImplicit   (* Mettre mkMeta ?? *)
 
 let evar_define isevars (ev,argsv) rhs =
-  if occur_evar ev rhs then error_occur_check empty_env ev rhs;
+  if occur_evar ev rhs
+  then error_occur_check empty_env (evars_of isevars) ev rhs;
   let args = List.map keep_rels_and_vars (Array.to_list argsv) in 
   let evd = ise_map isevars ev in
   (* the substitution to invert *)
@@ -407,7 +447,7 @@ let solve_refl conv_algo env isevars ev argsv1 argsv2 =
 
 (* Rq: uncomplete algorithm if pbty = CONV_X_LEQ ! *)
 let solve_simple_eqn conv_algo env isevars (pbty,(n1,args1 as ev1),t2) =
-  let t2 = nf_ise1 isevars.evars t2 in
+  let t2 = nf_evar isevars.evars t2 in
   let lsp = match kind_of_term t2 with
     | IsEvar (n2,args2 as ev2)
         when not (Evd.is_defined isevars.evars n2) ->
@@ -462,16 +502,17 @@ let mk_valcon c = Some c
 let split_tycon loc env isevars = function
   | None -> None,None
   | Some c ->
-      let t = whd_betadeltaiota env isevars.evars c in
+      let sigma = evars_of isevars in
+      let t = whd_betadeltaiota env sigma c in
       match kind_of_term t with
         | IsProd (na,dom,rng) -> Some dom, Some rng
 	| _ ->
 	    if ise_undefined isevars t then
-	      let (sigma,dom,rng) = split_evar_to_arrow isevars.evars t in
-	      isevars.evars <- sigma;
+	      let (sigma',dom,rng) = split_evar_to_arrow sigma t in
+	      evars_reset_evd sigma' isevars;
 	      Some dom, Some rng
 	    else
-	      error_not_product_loc loc env c
+	      error_not_product_loc loc env sigma c
 
 let valcon_of_tycon x = x
 
diff --git a/pretyping/evarutil.mli b/pretyping/evarutil.mli
index c31b57a4a..0295b7dfe 100644
--- a/pretyping/evarutil.mli
+++ b/pretyping/evarutil.mli
@@ -19,6 +19,24 @@ open Reduction
 
 (*s This modules provides useful functions for unification modulo evars *)
 
+(* [whd_ise] raise [Uninstantiated_evar] if an evar remains uninstantiated; *)
+(* *[whd_evar]* and *[nf_evar]* leave uninstantiated evar as is *)
+
+val nf_evar : 'a Evd.evar_map -> constr -> constr
+val j_nf_evar : 'a Evd.evar_map -> unsafe_judgment -> unsafe_judgment
+val jl_nf_evar :
+  'a Evd.evar_map -> unsafe_judgment list -> unsafe_judgment list
+val jv_nf_evar :
+  'a Evd.evar_map -> unsafe_judgment array -> unsafe_judgment array
+val tj_nf_evar :
+  'a Evd.evar_map -> unsafe_type_judgment -> unsafe_type_judgment
+
+(* Replacing all evars *)
+exception Uninstantiated_evar of int
+val whd_ise : 'a evar_map -> constr -> constr
+val whd_castappevar : 'a evar_map -> constr -> constr
+
+(* Creating new existential variables *)
 val new_evar : unit -> evar
 val new_evar_in_sign : env -> constr
 
diff --git a/pretyping/pretype_errors.ml b/pretyping/pretype_errors.ml
index f35b1b10b..4d6af242b 100644
--- a/pretyping/pretype_errors.ml
+++ b/pretyping/pretype_errors.ml
@@ -14,6 +14,7 @@ open Term
 open Environ
 open Type_errors
 open Rawterm
+open Inductive
 
 type ml_case_error =
   | MlCaseAbsurd
@@ -21,7 +22,7 @@ type ml_case_error =
 
 type pretype_error =
   (* Old Case *)
-  | MlCase of ml_case_error
+  | MlCase of ml_case_error * inductive_type * unsafe_judgment
   | CantFindCaseType of constr
   (* Unification *)
   | OccurCheck of int * constr
@@ -33,58 +34,104 @@ type pretype_error =
 
 exception PretypeError of env * pretype_error
 
-let raise_pretype_error (loc,ctx,te) =
-  Stdpp.raise_with_loc loc (PretypeError(ctx,te))
+(* 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 raise_located_type_error (loc,k,ctx,te) =
-  Stdpp.raise_with_loc loc (TypeError(k,ctx,te))
+let nf_evar sigma = Reduction.local_strong (whd_evar sigma)
+let j_nf_evar sigma j = 
+  { uj_val = nf_evar sigma j.uj_val;
+    uj_type = nf_evar sigma j.uj_type }
+let jl_nf_evar sigma jl = List.map (j_nf_evar sigma) jl
+let jv_nf_evar sigma = Array.map (j_nf_evar sigma)
+let tj_nf_evar sigma {utj_val=v;utj_type=t} =
+  {utj_val=type_app (nf_evar sigma) v;utj_type=t}
 
-let error_cant_find_case_type_loc loc env expr =
-  raise_pretype_error (loc, env, CantFindCaseType expr)
 
-let error_ill_formed_branch_loc loc k env c i actty expty =
-  raise_located_type_error (loc, k, env, IllFormedBranch (c,i,actty,expty))
+let env_ise sigma env =
+  map_context (nf_evar sigma) env
 
-let error_actual_type_loc loc env c actty expty =
-  raise_located_type_error (loc, CCI, env, ActualType (c,actty,expty))
 
-let error_cant_apply_not_functional_loc loc env rator randl =
+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 error_actual_type_loc loc env sigma {uj_val=c;uj_type=actty} expty =
+  raise_located_type_error
+    (loc, CCI, env, sigma,
+     ActualType (c,nf_evar sigma actty, nf_evar sigma expty))
+
+let error_cant_apply_not_functional_loc loc env sigma rator randl =
+  raise_located_type_error
+    (loc, CCI, env, sigma,
+    CantApplyNonFunctional (j_nf_evar sigma rator, jl_nf_evar sigma randl))
+
+let error_cant_apply_bad_type_loc loc env sigma (n,c,t) rator randl =
   raise_located_type_error
-    (loc,CCI,env, CantApplyNonFunctional (rator,randl))
+    (loc, CCI, env, sigma,
+     CantApplyBadType
+       ((n,nf_evar sigma c, nf_evar sigma t),
+        j_nf_evar sigma rator, jl_nf_evar sigma randl))
 
-let error_cant_apply_bad_type_loc loc env t rator randl =
-  raise_located_type_error (loc, CCI, env, CantApplyBadType (t,rator,randl))
+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 k env c i actty expty =
-  raise (TypeError (k, env, IllFormedBranch (c,i,actty,expty)))
+let error_ill_formed_branch_loc loc k 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,
+     IllFormedBranch (nf_evar sigma c,i,simp actty, simp expty))
 
-let error_number_branches_loc loc k env c ct expn =
-  raise_located_type_error (loc, k, env, NumberBranches (c,ct,expn))
+let error_number_branches_loc loc k env sigma cj expn =
+  raise_located_type_error
+    (loc, k, env, sigma,
+     NumberBranches (j_nf_evar sigma cj, expn))
 
-let error_case_not_inductive_loc loc k env c ct =
-  raise_located_type_error (loc, k, env, CaseNotInductive (c,ct))
+let error_case_not_inductive_loc loc k env sigma cj =
+  raise_located_type_error
+    (loc, k, env, sigma, CaseNotInductive (j_nf_evar sigma cj))
 
+let error_ill_typed_rec_body_loc loc k env sigma i na jl tys =
+  raise_located_type_error
+    (loc, k, env, sigma,
+     IllTypedRecBody (i,na,jv_nf_evar sigma jl,
+                      Array.map (nf_evar sigma) tys))
 
-(*s Implicit arguments synthesis errors *)
+(*s Implicit arguments synthesis errors. It is hard to find
+    a precise location. *)
 
-let error_occur_check env ev c =
-  raise (PretypeError (env, OccurCheck (ev,c)))
+let error_occur_check env sigma ev c =
+  let c = nf_evar sigma c in
+  raise (PretypeError (env_ise sigma env, OccurCheck (ev,c)))
 
-let error_not_clean env ev c =
-  raise (PretypeError (env, NotClean (ev,c)))
+let error_not_clean env sigma ev c =
+  let c = nf_evar sigma c in
+  raise (PretypeError (env_ise sigma env, NotClean (ev,c)))
 
 (*s Ml Case errors *)
 
-let error_ml_case_loc loc env mes =
-  raise_pretype_error (loc, env, MlCase mes)
+let error_ml_case_loc loc env sigma mes indt j =
+  raise_pretype_error
+    (loc, env, sigma, MlCase (mes, indt, j_nf_evar sigma j))
 
 (*s Pretyping errors *)
 
-let error_var_not_found_loc loc s =
-  raise_pretype_error (loc, Global.env() (*bidon*), VarNotFound s)
+let error_unexpected_type_loc loc env sigma actty expty =
+  raise_pretype_error
+    (loc, env, sigma,
+     UnexpectedType (nf_evar sigma actty, nf_evar sigma expty))
+
+let error_not_product_loc loc env sigma c =
+  raise_pretype_error (loc, env, sigma, NotProduct (nf_evar sigma c))
 
-let error_unexpected_type_loc loc env actty expty =
-  raise_pretype_error (loc, env, UnexpectedType (actty, expty))
+(*s Error in conversion from AST to rawterms *)
 
-let error_not_product_loc loc env c =
-  raise_pretype_error (loc, env, NotProduct c)
+let error_var_not_found_loc loc s =
+  raise_pretype_error (loc, empty_env, Evd.empty, VarNotFound s)
diff --git a/pretyping/pretype_errors.mli b/pretyping/pretype_errors.mli
index 717191aa8..90d90120e 100644
--- a/pretyping/pretype_errors.mli
+++ b/pretyping/pretype_errors.mli
@@ -14,8 +14,8 @@ open Names
 open Term
 open Sign
 open Environ
-open Type_errors
 open Rawterm
+open Inductive
 (*i*)
 
 (*s The type of errors raised by the pretyper *)
@@ -26,7 +26,7 @@ type ml_case_error =
 
 type pretype_error =
   (* Old Case *)
-  | MlCase of ml_case_error
+  | MlCase of ml_case_error * inductive_type * unsafe_judgment
   | CantFindCaseType of constr
   (* Unification *)
   | OccurCheck of int * constr
@@ -38,42 +38,67 @@ type pretype_error =
 
 exception PretypeError of env * pretype_error
 
-val error_cant_find_case_type_loc :
-  loc -> env -> constr -> 'a
+(* Presenting terms without solved evars *)
+val nf_evar : 'a Evd.evar_map -> constr -> constr
+val j_nf_evar : 'a Evd.evar_map -> unsafe_judgment -> unsafe_judgment
+val jl_nf_evar :
+  'a Evd.evar_map -> unsafe_judgment list -> unsafe_judgment list
+val jv_nf_evar :
+  'a Evd.evar_map -> unsafe_judgment array -> unsafe_judgment array
+val tj_nf_evar :
+  'a Evd.evar_map -> unsafe_type_judgment -> unsafe_type_judgment
 
-val error_ill_formed_branch_loc : 
-  loc -> path_kind -> env -> constr -> int -> constr -> constr -> 'b
 
+(* Raising errors *)
 val error_actual_type_loc :
-  loc -> env -> constr -> constr -> constr -> 'b
+  loc -> env -> 'a Evd.evar_map -> unsafe_judgment -> constr -> 'b
 
 val error_cant_apply_not_functional_loc : 
-  loc -> env -> unsafe_judgment -> unsafe_judgment list -> 'b
+  loc -> env -> 'a Evd.evar_map ->
+      unsafe_judgment -> unsafe_judgment list -> 'b
 
 val error_cant_apply_bad_type_loc : 
-  loc -> env -> int * constr * constr -> 
+  loc -> env -> 'a Evd.evar_map -> int * constr * constr -> 
       unsafe_judgment -> unsafe_judgment list -> 'b
 
-val error_number_branches_loc : 
-  loc -> path_kind -> env -> constr -> constr -> int -> 'b
+val error_cant_find_case_type_loc :
+  loc -> env -> 'a Evd.evar_map -> constr -> 'b
 
 val error_case_not_inductive_loc :
-  loc -> path_kind -> env -> constr -> constr -> 'b
+  loc -> path_kind -> env -> 'a Evd.evar_map -> unsafe_judgment -> 'b
+
+val error_ill_formed_branch_loc : 
+  loc -> path_kind -> env -> 'a Evd.evar_map ->
+      constr -> int -> constr -> constr -> 'b
+
+val error_number_branches_loc : 
+  loc -> path_kind -> env -> 'a Evd.evar_map ->
+      unsafe_judgment -> int -> 'b
+
+val error_ill_typed_rec_body_loc :
+  loc -> path_kind -> env -> 'a Evd.evar_map ->
+      int -> name array -> unsafe_judgment array -> types array -> 'b
 
 (*s Implicit arguments synthesis errors *)
 
-val error_occur_check : env -> int -> constr -> 'a
+val error_occur_check : env -> 'a Evd.evar_map -> int -> constr -> 'b
 
-val error_not_clean : env -> int -> constr -> 'a
+val error_not_clean : env -> 'a Evd.evar_map -> int -> constr -> 'b
 
 (*s Ml Case errors *)
 
-val error_ml_case_loc : loc -> env -> ml_case_error -> 'a
+val error_ml_case_loc :
+  loc -> env -> 'a Evd.evar_map ->
+      ml_case_error -> inductive_type -> unsafe_judgment -> 'b
 
 (*s Pretyping errors *)
 
-val error_var_not_found_loc : loc -> identifier -> 'a
+val error_unexpected_type_loc :
+  loc -> env -> 'a Evd.evar_map -> constr -> constr -> 'b
+
+val error_not_product_loc :
+  loc -> env -> 'a Evd.evar_map -> constr -> 'b
 
-val error_unexpected_type_loc : loc -> env -> constr -> constr -> 'b
+(*s Error in conversion from AST to rawterms *)
 
-val error_not_product_loc : loc -> env -> constr -> 'a
+val error_var_not_found_loc : loc -> identifier -> 'b
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index c06e0d580..d2855a64f 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -37,17 +37,18 @@ let lift_context n l =
   let k = List.length l in 
   list_map_i (fun i (name,c) -> (name,liftn n (k-i) c)) 0 l
 
-let transform_rec loc env sigma (p,c,lf) (indt,pt) = 
+let transform_rec loc env sigma (pj,c,lf) indt = 
+  let p = pj.uj_val in
   let (indf,realargs) = dest_ind_type indt in
   let (mispec,params) = dest_ind_family indf in
   let mI = mkMutInd (mis_inductive mispec) in
   let recargs = mis_recarg mispec in
   let tyi = mis_index mispec in
   if Array.length lf <> mis_nconstr mispec then 
-    error_number_branches_loc loc CCI env c
-      (mkAppliedInd indt) (mis_nconstr mispec);
+    (let cj = {uj_val=c; uj_type=mkAppliedInd indt} in
+     error_number_branches_loc loc CCI env sigma cj (mis_nconstr mispec));
   if mis_is_recursive_subset [tyi] mispec then
-    let (dep,_) = find_case_dep_nparams env sigma (c,p) indf pt in 
+    let (dep,_) = find_case_dep_nparams env sigma (c,pj) indf in 
     let init_depFvec i = if i = tyi then Some(dep,mkRel 1) else None in
     let depFvec = Array.init (mis_ntypes mispec) init_depFvec in
     (* build now the fixpoint *)
@@ -107,44 +108,27 @@ let mt_evd = Evd.empty
 
 let vect_lift_type = Array.mapi (fun i t -> type_app (lift i) t)
 
-let j_nf_ise sigma {uj_val=v;uj_type=t} =
-  {uj_val=nf_ise1 sigma v;uj_type=type_app (nf_ise1 sigma) t}
-
-let jv_nf_ise sigma = Array.map (j_nf_ise sigma)
-
-let tj_nf_ise sigma {utj_val=v;utj_type=t} =
-  {utj_val=type_app (nf_ise1 sigma) v;utj_type=t}
-
 (* Utilisé pour inférer le prédicat des Cases *)
 (* Semble exagérement fort *)
 (* Faudra préférer une unification entre les types de toutes les clauses *)
 (* et autoriser des ? à rester dans le résultat de l'unification *)
 
-let evar_type_fixpoint env isevars lna lar vdefj =
+let evar_type_fixpoint loc env isevars lna lar vdefj =
   let lt = Array.length vdefj in 
     if Array.length lar = lt then 
       for i = 0 to lt-1 do 
         if not (the_conv_x_leq env isevars
 		  (vdefj.(i)).uj_type
 		  (lift lt lar.(i))) then
-          error_ill_typed_rec_body CCI env i lna 
-	    (jv_nf_ise (evars_of isevars) vdefj) 
-	    (Array.map (type_app (nf_ise1 (evars_of isevars))) lar)
+          error_ill_typed_rec_body_loc loc CCI env (evars_of isevars)
+            i lna vdefj lar
       done
 
-let wrong_number_of_cases_message loc env isevars (c,ct) expn = 
-  let c = nf_ise1 (evars_of isevars) c
-  and ct = nf_ise1 (evars_of isevars) ct in
-  error_number_branches_loc loc CCI env c ct expn
-
 let check_branches_message loc env isevars c (explft,lft) = 
   for i = 0 to Array.length explft - 1 do
     if not (the_conv_x_leq env isevars lft.(i) explft.(i)) then 
-      let c = nf_ise1 (evars_of isevars) c
-      and lfi = nf_betaiota env (evars_of isevars)
-        (nf_ise1 (evars_of isevars) lft.(i)) in
-      error_ill_formed_branch_loc loc CCI env c i lfi 
-	(nf_betaiota env (evars_of isevars) explft.(i))
+      let sigma = evars_of isevars in
+      error_ill_formed_branch_loc loc CCI env sigma c i lft.(i) explft.(i)
   done
 
 (* coerce to tycon if any *)
@@ -275,7 +259,7 @@ let rec pretype tycon env isevars lvar lmeta = function
              pretype (mk_tycon (lift nbfix (larj.(i).utj_val)))
                newenv isevars lvar lmeta def)
           vdef in
-      evar_type_fixpoint env isevars names lara vdefj;
+      evar_type_fixpoint loc env isevars names lara vdefj;
       let fixj =
 	match fixkind with
 	  | RFix (vn,i as vni) ->
@@ -310,14 +294,10 @@ let rec pretype tycon env isevars lvar lmeta = function
 		  apply_rec env (n+1) newresj rest
 
 	      | _ ->
-		  let j_nf_ise env sigma {uj_val=v;uj_type=t} =
-		    { uj_val = nf_ise1 sigma v; 
-		      uj_type = nf_ise1 sigma t } in
 		  let hj = pretype empty_tycon env isevars lvar lmeta c in
 		  error_cant_apply_not_functional_loc 
-		    (Rawterm.join_loc floc argloc) env
-	      	    (j_nf_ise env (evars_of isevars) resj)
-		    [j_nf_ise env (evars_of isevars) hj]
+		    (Rawterm.join_loc floc argloc) env (evars_of isevars)
+	      	    resj [hj]
 
       in let resj = apply_rec env 1 fj args in
       (*
@@ -365,9 +345,8 @@ let rec pretype tycon env isevars lvar lmeta = function
       let cj = pretype empty_tycon env isevars lvar lmeta c in
       let (IndType (indf,realargs) as indt) = 
 	try find_rectype env (evars_of isevars) cj.uj_type
-	with Induc -> error_case_not_inductive CCI env
-	    (nf_ise1 (evars_of isevars) cj.uj_val)
-            (nf_ise1 (evars_of isevars) cj.uj_type) in
+	with Induc ->
+          error_case_not_inductive_loc loc CCI env (evars_of isevars) cj in
       let pj = match po with
 	| Some p -> pretype empty_tycon env isevars lvar lmeta p
 	| None -> 
@@ -379,17 +358,17 @@ let rec pretype tycon env isevars lvar lmeta = function
 	      let expbr = Cases.branch_scheme env isevars isrec indf in
 	      let rec findtype i =
 		if i >= Array.length lf
-		then error_cant_find_case_type_loc loc env cj.uj_val
+		then
+                  let sigma = evars_of isevars in
+                  error_cant_find_case_type_loc loc env sigma cj.uj_val
 		else
 		  try
 		    let expti = expbr.(i) in
 		    let fj =
 		      pretype (mk_tycon expti) env isevars lvar lmeta lf.(i) in
-		    let efjt = nf_ise1 (evars_of isevars) fj.uj_type in 
 		    let pred = 
 		      Cases.pred_case_ml_onebranch
-                        loc env (evars_of isevars) isrec indt
-			(i,fj.uj_val,efjt) in
+                        loc env (evars_of isevars) isrec indt (i,fj) in
 		    if has_undefined_isevars isevars pred then findtype (i+1)
 		    else 
 		      let pty =
@@ -398,33 +377,31 @@ let rec pretype tycon env isevars lvar lmeta = function
 			uj_type = pty }
 		  with UserError _ -> findtype (i+1) in
 	      findtype 0 in
-
-      let evalPt = nf_ise1 (evars_of isevars) pj.uj_type in
+      let pj = j_nf_evar (evars_of isevars) pj in
 
       let (dep,_) = find_case_dep_nparams env (evars_of isevars)
-        (cj.uj_val,pj.uj_val) indf evalPt in
+        (cj.uj_val,pj) indf in
 
-      let (p,pt) =
-	if dep then (pj.uj_val, evalPt) else
+      let pj =
+	if dep then pj else
 	  let n = List.length realargs in
 	  let rec decomp n p =
 	    if n=0 then p else
 	      match kind_of_term p with
 		| IsLambda (_,_,c) -> decomp (n-1) c
 		| _ -> decomp (n-1) (applist (lift 1 p, [mkRel 1])) in
-	  let sign,s = decompose_prod_n n evalPt in
+	  let sign,s = decompose_prod_n n pj.uj_type in
 	  let ind = build_dependent_inductive indf in
 	  let s' = mkProd (Anonymous, ind, s) in
 	  let ccl = lift 1 (decomp n pj.uj_val) in
 	  let ccl' = mkLambda (Anonymous, ind, ccl) in
-	  (lam_it ccl' sign, prod_it s' sign) in
+	  {uj_val=lam_it ccl' sign; uj_type=prod_it s' sign} in
       let (bty,rsty) =
 	Indrec.type_rec_branches
-          isrec env (evars_of isevars) indt pt p cj.uj_val in
+          isrec env (evars_of isevars) indt pj cj.uj_val in
       if Array.length bty <> Array.length lf then
-	wrong_number_of_cases_message loc env isevars 
-	  (cj.uj_val,nf_ise1 (evars_of isevars) cj.uj_type)
-	  (Array.length bty)
+	error_number_branches_loc loc CCI env (evars_of isevars) 
+	  cj (Array.length bty)
       else
 	let lfj =
 	  array_map2
@@ -436,11 +413,12 @@ let rec pretype tycon env isevars lvar lmeta = function
 	let v =
 	  if isrec
 	  then 
-	    transform_rec loc env (evars_of isevars)(p,cj.uj_val,lfv) (indt,pt)
+	    transform_rec loc env (evars_of isevars)(pj,cj.uj_val,lfv) indt
 	  else
 	    let mis,_ = dest_ind_family indf in
 	    let ci = make_default_case_info mis in
-	    mkMutCase (ci, p, cj.uj_val, Array.map (fun j-> j.uj_val) lfj)
+	    mkMutCase (ci, pj.uj_val, cj.uj_val,
+                       Array.map (fun j-> j.uj_val) lfj)
 	in
 	{uj_val = v;
 	 uj_type = rsty }
@@ -475,16 +453,17 @@ and pretype_type valcon env isevars lvar lmeta = function
 	| Some v ->
 	    if the_conv_x_leq env isevars v tj.utj_val then tj
 	    else
-	      error_unexpected_type_loc (loc_of_rawconstr c) env tj.utj_val v
+	      error_unexpected_type_loc
+                (loc_of_rawconstr c) env (evars_of isevars) tj.utj_val v
 
 
 let unsafe_infer tycon isevars env lvar lmeta constr =
   let j = pretype tycon env isevars lvar lmeta constr in
-  j_nf_ise (evars_of isevars) j
+  j_nf_evar (evars_of isevars) j
 
 let unsafe_infer_type valcon isevars env lvar lmeta constr =
   let tj = pretype_type valcon env isevars lvar lmeta constr in
-  tj_nf_ise (evars_of isevars) tj
+  tj_nf_evar (evars_of isevars) tj
 
 (* If fail_evar is false, [process_evars] builds a meta_map with the
    unresolved Evar that were not in initial sigma; otherwise it fail
diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml
index 72ebb6626..f3f010e5e 100644
--- a/pretyping/tacred.ml
+++ b/pretyping/tacred.ml
@@ -342,7 +342,7 @@ let rec red_elim_const env sigma ref largs =
 	let co = construct_const env sigma in
 	(match reduce_fix_use_function f co (destFix d) lrest with
 	   | NotReducible -> raise Redelimination
-	   | Reduced (c,rest) -> (nf_beta env sigma c, rest))
+	   | Reduced (c,rest) -> (nf_beta c, rest))
     | EliminationMutualFix (min,refgoal,refinfos)
 	when stack_args_size largs >= min ->
 	let rec descend ref args =
@@ -358,7 +358,7 @@ let rec red_elim_const env sigma ref largs =
 	let co = construct_const env sigma in
 	(match reduce_fix_use_function f co (destFix d) lrest with
 	   | NotReducible -> raise Redelimination
-	   | Reduced (c,rest) -> (nf_beta env sigma c, rest))
+	   | Reduced (c,rest) -> (nf_beta c, rest))
     | _ -> raise Redelimination
 
 and construct_const env sigma = 
@@ -413,7 +413,7 @@ let internal_red_product env sigma c =
 	     | None -> raise Redelimination
 	     | Some c -> c)
       | _ -> raise Redelimination
-  in nf_betaiota env sigma (redrec env c)
+  in nf_betaiota (redrec env c)
 
 let red_product env sigma c = 
   try internal_red_product env sigma c
@@ -609,7 +609,7 @@ let unfoldoccs env sigma (occl,name) c =
     | []  -> unfold env sigma name c
     | l -> 
         match substlin env name 1 (Sort.list (<) l) c with
-          | (_,[],uc) -> nf_betaiota env sigma uc
+          | (_,[],uc) -> nf_betaiota uc
           | (1,_,_) -> error ((string_of_evaluable_ref name)^" does not occur")
           | _ -> error ("bad occurrence numbers of "
 			^(string_of_evaluable_ref name))
@@ -633,9 +633,9 @@ let fold_commands cl env sigma c =
 let cbv_norm_flags flags env sigma t =
   cbv_norm (create_cbv_infos flags env sigma) t
 
-let cbv_beta env = cbv_norm_flags beta env
-let cbv_betaiota env = cbv_norm_flags betaiota env
-let cbv_betadeltaiota env =  cbv_norm_flags betadeltaiota env
+let cbv_beta = cbv_norm_flags beta empty_env Evd.empty
+let cbv_betaiota = cbv_norm_flags betaiota empty_env Evd.empty
+let cbv_betadeltaiota env sigma =  cbv_norm_flags betadeltaiota env sigma
 
 let compute = cbv_betadeltaiota
 
@@ -725,7 +725,7 @@ let reduce_to_mind env sigma t =
 	  elimrec (push_rel_assum (n,t) env) t' ((n,None,ty)::l)
       | _ -> 
           (try 
-	     let t' = nf_betaiota env sigma (one_step_reduce env sigma t) in 
+	     let t' = nf_betaiota (one_step_reduce env sigma t) in 
 	     elimrec env t' l
            with UserError _ -> errorlabstrm "tactics__reduce_to_mind"
                [< 'sTR"Not an inductive product." >])
diff --git a/pretyping/tacred.mli b/pretyping/tacred.mli
index 4d248983f..c75f33794 100644
--- a/pretyping/tacred.mli
+++ b/pretyping/tacred.mli
@@ -43,8 +43,8 @@ val pattern_occs : (int list * constr * constr) list -> 'a reduction_function
 
 (* Call by value strategy (uses Closures) *)
 val cbv_norm_flags : Closure.flags -> 'a reduction_function
-  val cbv_beta : 'a reduction_function
-  val cbv_betaiota : 'a reduction_function
+  val cbv_beta : local_reduction_function
+  val cbv_betaiota : local_reduction_function
   val cbv_betadeltaiota : 'a reduction_function
   val compute : 'a reduction_function  (* = [cbv_betadeltaiota] *)
 
diff --git a/pretyping/typing.ml b/pretyping/typing.ml
index f78216336..f9110c62a 100644
--- a/pretyping/typing.ml
+++ b/pretyping/typing.ml
@@ -38,7 +38,7 @@ let rec execute mf env sigma cstr =
 	{ uj_val = cstr; uj_type = jty }
 	
     | IsRel n -> 
-	relative env sigma n
+	relative env n
 
     | IsVar id -> 
       (try
@@ -158,7 +158,7 @@ let unsafe_machine env sigma constr =
 
 let type_of env sigma c = 
   let j = safe_machine env sigma c in 
-  nf_betaiota env sigma (body_of_type j.uj_type)
+  nf_betaiota (body_of_type j.uj_type)
 
 (* The typed type of a judgment. *)