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

42 files changed, 449 insertions, 418 deletions

diff --git a/contrib/correctness/ptactic.ml b/contrib/correctness/ptactic.ml
index a4b62c53c..66633277a 100644
--- a/contrib/correctness/ptactic.ml
+++ b/contrib/correctness/ptactic.ml
@@ -220,7 +220,7 @@ let correctness s p opttac =
   let env = Global.env () in
   let sign = Global.named_context () in
   let sigma = Evd.empty in
-  let cty = Reduction.nf_betaiota env sigma cty in
+  let cty = Reduction.nf_betaiota cty in
   let id = id_of_string s in 
   start_proof id Declare.NeverDischarge sign cty;
   Penv.new_edited id (v,p);
diff --git a/contrib/interface/centaur.ml b/contrib/interface/centaur.ml
index f48f04e7c..6e1555d59 100644
--- a/contrib/interface/centaur.ml
+++ b/contrib/interface/centaur.ml
@@ -289,7 +289,7 @@ let ct_print_eval ast red_fun env evd judg =
 let {uj_val=value; uj_type=typ} = judg in
 let nvalue = red_fun value
 (* // Attention , ici il faut peut être utiliser des environnemenst locaux *)
-and ntyp = nf_betaiota env evd typ in
+and ntyp = nf_betaiota typ in
 (ctf_SearchResults !global_request_id,
  Some (P_pl
   (CT_premises_list
diff --git a/contrib/xml/xmlcommand.ml b/contrib/xml/xmlcommand.ml
index 5f23c1d64..95a93cde7 100644
--- a/contrib/xml/xmlcommand.ml
+++ b/contrib/xml/xmlcommand.ml
@@ -265,8 +265,7 @@ let print_term inner_types l env csr =
 
   let inner_type_display env term =
    let type_of_term =
-    Reduction.nf_betaiota env (Evd.empty)
-     (R.get_type_of env (Evd.empty) term)
+    Reduction.nf_betaiota (R.get_type_of env (Evd.empty) term)
    in
     match R.get_sort_of env (Evd.empty) type_of_term with
        T.Prop T.Null -> InnerProp type_of_term
diff --git a/dev/base_include b/dev/base_include
index 2515cabd3..8ef9fc5ba 100644
--- a/dev/base_include
+++ b/dev/base_include
@@ -1,30 +1,6 @@
 
 (* File to include to get some Coq facilities under the ocaml toplevel.
-   This file is loaded by include.ml *)
-
-(* We only assume that the variable COQTOP is set *)
-let src_dir =
-  let coqtop = try Sys.getenv "COQTOP" with Not_found -> "." in
-  let coqtop = 
-    if Sys.file_exists coqtop then 
-      coqtop
-    else begin
-      print_endline ("Cannot find the sources in "^coqtop);
-      print_string "Where are they ? ";
-      read_line ()
-    end 
-  in
-  let add_dir dl = 
-    Topdirs.dir_directory (List.fold_left Filename.concat coqtop dl) 
-  in
-  List.iter add_dir
-    [ [ "config" ]; [ "dev" ]; [ "lib" ]; [ "kernel" ]; [ "library" ]; 
-      [ "pretyping" ]; [ "parsing" ]; [ "proofs" ]; [ "tactics" ];
-      [ "toplevel" ] ];
-  coqtop
-;;
-(* Now Coq_config.cmi is accessible *)
-Topdirs.dir_directory Coq_config.camlp4lib;;
+   This file is loaded by include *)
 
 #use "top_printers.ml";;
 
diff --git a/kernel/cooking.ml b/kernel/cooking.ml
index 2ad841d03..0a023fb9c 100644
--- a/kernel/cooking.ml
+++ b/kernel/cooking.ml
@@ -110,7 +110,7 @@ let modify_opers replfun absfun (constl,indl,cstrl) =
 let expmod_constr oldenv modlist c =
   let sigma = Evd.empty in
   let simpfun = 
-    if modlist = ([],[],[]) then fun x -> x else nf_betaiota oldenv sigma in
+    if modlist = ([],[],[]) then fun x -> x else nf_betaiota in
   let expfun cst = 
     try 
       constant_value oldenv cst
diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml
index e67aff002..344ca87fb 100644
--- a/kernel/indtypes.ml
+++ b/kernel/indtypes.ml
@@ -165,7 +165,7 @@ let abstract_mind_lc env ntyps npars lc =
       list_tabulate
 	(function i -> lambda_implicit_lift npars (mkRel (i+1))) ntyps 
     in 
-    Array.map (compose (nf_beta env Evd.empty) (substl make_abs)) lc
+    Array.map (compose nf_beta (substl make_abs)) lc
 
 let listrec_mconstr env ntypes hyps nparams i indlc =
   let nhyps = List.length hyps in
diff --git a/kernel/reduction.ml b/kernel/reduction.ml
index 312ee83d2..5b602bfdc 100644
--- a/kernel/reduction.ml
+++ b/kernel/reduction.ml
@@ -81,9 +81,9 @@ let rec strong_prodspine redfun c =
 let clos_norm_flags flgs env sigma t =
   norm_val (create_clos_infos flgs env sigma) (inject t)
 
-let nf_beta env = clos_norm_flags beta env
-let nf_betaiota env = clos_norm_flags betaiota env
-let nf_betadeltaiota env =  clos_norm_flags betadeltaiota env
+let nf_beta = clos_norm_flags beta empty_env Evd.empty
+let nf_betaiota = clos_norm_flags betaiota empty_env Evd.empty
+let nf_betadeltaiota env sigma =  clos_norm_flags betadeltaiota env sigma
 
 (* lazy weak head reduction functions *)
 let whd_flags flgs env sigma t =
@@ -1088,43 +1088,3 @@ let is_info_type env sigma t =
   (s = Prop Pos) ||
   (s <> Prop Null && 
    try info_arity env sigma t.utj_val with IsType -> true)
-
-(* 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
-
-
-(* 2- undefined existentials are left unchanged *)
-let rec whd_ise1 sigma c =
-  match kind_of_term c with
-    | IsEvar (ev,args) when Evd.in_dom sigma ev & Evd.is_defined sigma ev ->
-	whd_ise1 sigma (existential_value sigma (ev,args))
-    | _ -> collapse_appl c
-
-let nf_ise1 sigma = local_strong (whd_ise1 sigma)
-
-(* A form of [whd_ise1] with type "reduction_function" *)
-let whd_evar env = whd_ise1
-
-(* 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)
diff --git a/kernel/reduction.mli b/kernel/reduction.mli
index ae0640aef..a32f36a6a 100644
--- a/kernel/reduction.mli
+++ b/kernel/reduction.mli
@@ -58,8 +58,8 @@ val stacklam : (state -> 'a) -> constr list -> constr -> constr stack -> 'a
 
 val clos_norm_flags : Closure.flags -> 'a reduction_function
 (* Same as [(strong whd_beta[delta][iota])], but much faster on big terms *) 
-val nf_beta : 'a reduction_function
-val nf_betaiota : 'a reduction_function
+val nf_beta : local_reduction_function
+val nf_betaiota : local_reduction_function
 val nf_betadeltaiota : 'a reduction_function
 
 (* Lazy strategy, weak head reduction *)
@@ -101,7 +101,6 @@ val whd_betadeltaeta : 'a reduction_function
 val whd_betadeltaiotaeta_stack : 'a stack_reduction_function
 val whd_betadeltaiotaeta_state : 'a state_reduction_function
 val whd_betadeltaiotaeta : 'a reduction_function
-val whd_evar : 'a reduction_function
 
 val beta_applist : constr * constr list -> constr
 
@@ -192,16 +191,6 @@ val whd_meta : (int * constr) list -> constr -> constr
 val plain_instance : (int * constr) list -> constr -> constr
 val instance : (int * constr) list -> constr -> constr
 
-(* [whd_ise] raise [Uninstantiated_evar] if an evar remains uninstantiated; *)
-(* *[whd_ise1]* is synonymous of *[whd_evar empty_env]* and *[nf_ise1]* of *)
-(* *[strong whd_evar empty_env]*: they leave uninstantiated evar as it *)
-
-val whd_ise1 : 'a evar_map -> constr -> constr
-val nf_ise1 : 'a evar_map -> constr -> constr
-exception Uninstantiated_evar of int
-val whd_ise : 'a evar_map -> constr -> constr
-val whd_castappevar : 'a evar_map -> constr -> constr
-
 (*s Obsolete Reduction Functions *)
 
 (*i
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index 7df425894..d2887cce8 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -90,7 +90,7 @@ let rec execute env cstr cu =
           (cast_rel env Evd.empty cj tj)
 
     | IsRel n -> 
-	(relative env Evd.empty n, cu)
+	(relative env n, cu)
 
     | IsVar id -> 
 	(make_judge cstr (lookup_named_type id env), cu)
diff --git a/kernel/type_errors.ml b/kernel/type_errors.ml
index 320a30369..05b6e2675 100644
--- a/kernel/type_errors.ml
+++ b/kernel/type_errors.ml
@@ -13,6 +13,7 @@ open Names
 open Term
 open Sign
 open Environ
+open Reduction
 
 (* Type errors. *)
 
@@ -39,10 +40,10 @@ type type_error =
   | NotAType of unsafe_judgment
   | BadAssumption of constr
   | ReferenceVariables of identifier
-  | ElimArity of inductive * constr list * constr * constr * constr
+  | ElimArity of inductive * constr list * constr * unsafe_judgment
       * (constr * constr * string) option
-  | CaseNotInductive of constr * constr
-  | NumberBranches of constr * constr * int
+  | CaseNotInductive of unsafe_judgment
+  | NumberBranches of unsafe_judgment * int
   | IllFormedBranch of constr * int * constr * constr
   | Generalization of (name * types) * unsafe_judgment
   | ActualType of constr * constr * constr
@@ -55,11 +56,11 @@ type type_error =
 
 exception TypeError of path_kind * env * type_error
 
-let env_ise sigma env =
-  map_context (Reduction.nf_ise1 sigma) env
+let nfj {uj_val=c;uj_type=ct} =
+  {uj_val=c;uj_type=nf_betaiota ct}
 
-let error_unbound_rel k env sigma n =
-  raise (TypeError (k, env_ise sigma env, UnboundRel n))
+let error_unbound_rel k env n =
+  raise (TypeError (k, env, UnboundRel n))
 
 let error_not_type k env c =
   raise (TypeError (k, env, NotAType c))
@@ -70,20 +71,21 @@ let error_assumption k env c =
 let error_reference_variables k env id =
   raise (TypeError (k, env, ReferenceVariables id))
 
-let error_elim_arity k env ind aritylst c p pt okinds = 
-  raise (TypeError (k, env, ElimArity (ind,aritylst,c,p,pt,okinds)))
+let error_elim_arity k env ind aritylst c pj okinds = 
+  raise (TypeError (k, env, ElimArity (ind,aritylst,c,pj,okinds)))
 
-let error_case_not_inductive k env c ct = 
-  raise (TypeError (k, env, CaseNotInductive (c,ct)))
+let error_case_not_inductive k env j = 
+  raise (TypeError (k, env, CaseNotInductive j))
 
-let error_number_branches k env c ct expn =
-  raise (TypeError (k, env, NumberBranches (c,ct,expn)))
+let error_number_branches k env cj expn =
+  raise (TypeError (k, env, NumberBranches (nfj cj,expn)))
 
 let error_ill_formed_branch k env c i actty expty =
-  raise (TypeError (k, env, IllFormedBranch (c,i,actty,expty)))
+  raise (TypeError (k, env,
+    IllFormedBranch (c,i,nf_betaiota actty, nf_betaiota expty)))
 
-let error_generalization k env sigma nvar c =
-  raise (TypeError (k, env_ise sigma env, Generalization (nvar,c)))
+let error_generalization k env nvar c =
+  raise (TypeError (k, env, Generalization (nvar,c)))
 
 let error_actual_type k env c actty expty =
   raise (TypeError (k, env, ActualType (c,actty,expty)))
@@ -91,8 +93,8 @@ let error_actual_type k env c actty expty =
 let error_cant_apply_not_functional k env rator randl =
   raise (TypeError (k, env, CantApplyNonFunctional (rator,randl)))
 
-let error_cant_apply_bad_type k env sigma t rator randl =
-  raise(TypeError (k, env_ise sigma env, CantApplyBadType (t,rator,randl)))
+let error_cant_apply_bad_type k env t rator randl =
+  raise(TypeError (k, env, CantApplyBadType (t,rator,randl)))
 
 let error_ill_formed_rec_body k env why lna i vdefs =
   raise (TypeError (k, env, IllFormedRecBody (why,lna,i,vdefs)))
diff --git a/kernel/type_errors.mli b/kernel/type_errors.mli
index 277e5ca4e..11729171b 100644
--- a/kernel/type_errors.mli
+++ b/kernel/type_errors.mli
@@ -43,10 +43,10 @@ type type_error =
   | NotAType of unsafe_judgment
   | BadAssumption of constr
   | ReferenceVariables of identifier
-  | ElimArity of inductive * constr list * constr * constr * constr
+  | ElimArity of inductive * constr list * constr * unsafe_judgment
       * (constr * constr * string) option
-  | CaseNotInductive of constr * constr
-  | NumberBranches of constr * constr * int
+  | CaseNotInductive of unsafe_judgment
+  | NumberBranches of unsafe_judgment * int
   | IllFormedBranch of constr * int * constr * constr
   | Generalization of (name * types) * unsafe_judgment
   | ActualType of constr * constr * constr
@@ -59,44 +59,44 @@ type type_error =
 
 exception TypeError of path_kind * env * type_error
 
-val error_unbound_rel : path_kind -> env -> 'a Evd.evar_map -> int -> 'b
+val error_unbound_rel : path_kind -> env -> int -> 'a
 
-val error_not_type : path_kind -> env -> unsafe_judgment -> 'b
+val error_not_type : path_kind -> env -> unsafe_judgment -> 'a
 
-val error_assumption : path_kind -> env -> constr -> 'b
+val error_assumption : path_kind -> env -> constr -> 'a
  
-val error_reference_variables : path_kind -> env -> identifier -> 'b
+val error_reference_variables : path_kind -> env -> identifier -> 'a
 
 val error_elim_arity : 
   path_kind -> env -> inductive -> constr list -> constr 
-    -> constr -> constr -> (constr * constr * string) option -> 'b
+    -> unsafe_judgment -> (constr * constr * string) option -> 'a
 
 val error_case_not_inductive : 
-  path_kind -> env -> constr -> constr -> 'b
+  path_kind -> env -> unsafe_judgment -> 'a
 
 val error_number_branches : 
-  path_kind -> env -> constr -> constr -> int -> 'b
+  path_kind -> env -> unsafe_judgment -> int -> 'a
 
 val error_ill_formed_branch :
-  path_kind -> env -> constr -> int -> constr -> constr -> 'b
+  path_kind -> env -> constr -> int -> constr -> constr -> 'a
 
 val error_generalization :
-  path_kind -> env -> 'a Evd.evar_map -> name * types -> unsafe_judgment -> 'b
+  path_kind -> env -> name * types -> unsafe_judgment -> 'a
 
 val error_actual_type :
-  path_kind -> env -> constr -> constr -> constr -> 'b
+  path_kind -> env -> constr -> constr -> constr -> 'a
 
 val error_cant_apply_not_functional : 
-  path_kind -> env -> unsafe_judgment -> unsafe_judgment list -> 'b
+  path_kind -> env -> unsafe_judgment -> unsafe_judgment list -> 'a
 
 val error_cant_apply_bad_type : 
-  path_kind -> env -> 'a Evd.evar_map -> int * constr * constr -> 
-      unsafe_judgment -> unsafe_judgment list -> 'b
+  path_kind -> env -> int * constr * constr -> 
+      unsafe_judgment -> unsafe_judgment list -> 'a
 
 val error_ill_formed_rec_body :
-  path_kind -> env -> guard_error -> name array -> int -> constr array -> 'b
+  path_kind -> env -> guard_error -> name array -> int -> constr array -> 'a
 
 val error_ill_typed_rec_body  :
   path_kind -> env -> int -> name array -> unsafe_judgment array 
-    -> types array -> 'b
+    -> types array -> 'a
 
diff --git a/kernel/typeops.ml b/kernel/typeops.ml
index 37106b200..ecbd59636 100644
--- a/kernel/typeops.ml
+++ b/kernel/typeops.ml
@@ -84,13 +84,13 @@ let type_of_sort c =
 
 (* Type of a de Bruijn index. *)
 	  
-let relative env sigma n = 
+let relative env n = 
   try
     let (_,typ) = lookup_rel_type n env in
     { uj_val  = mkRel n;
       uj_type = type_app (lift n) typ }
   with Not_found -> 
-    error_unbound_rel CCI env sigma n
+    error_unbound_rel CCI env n
 
 (*
 let relativekey = Profile.declare_profile "relative";;
@@ -206,7 +206,7 @@ let apply_rel_list env sigma nocheck argjl funj =
 		   let cst' = Constraint.union cst c in
 		   apply_rec (n+1) (subst1 hj.uj_val c2) cst' restjl
 		 with NotConvertible -> 
-		   error_cant_apply_bad_type CCI env sigma
+		   error_cant_apply_bad_type CCI env
 		     (n,c1,body_of_type hj.uj_type)
 		     funj argjl)
 
@@ -289,7 +289,7 @@ let error_elim_expln env sigma kp ki =
 
 exception Arity of (constr * constr * string) option
 
-let is_correct_arity env sigma kelim (c,p) indf (pt,t) = 
+let is_correct_arity env sigma kelim (c,pj) indf t = 
   let rec srec (pt,t) u =
     let pt' = whd_betadeltaiota env sigma pt in
     let t' = whd_betadeltaiota env sigma t in
@@ -321,22 +321,22 @@ let is_correct_arity env sigma kelim (c,p) indf (pt,t) =
           else 
 	    raise (Arity (Some(pt',t',error_elim_expln env sigma pt' t')))
   in 
-  try srec (pt,t) Constraint.empty
+  try srec (pj.uj_type,t) Constraint.empty
   with Arity kinds ->
     let listarity =
       (List.map (make_arity env true indf) kelim)
       @(List.map (make_arity env false indf) kelim)
     in 
     let ind = mis_inductive (fst (dest_ind_family indf)) in
-    error_elim_arity CCI env ind listarity c p pt kinds
+    error_elim_arity CCI env ind listarity c pj kinds
 
 
-let find_case_dep_nparams env sigma (c,p) (IndFamily (mis,_) as indf) typP =
+let find_case_dep_nparams env sigma (c,pj) (IndFamily (mis,_) as indf) =
   let kelim = mis_kelim mis in
   let arsign,s = get_arity indf in
   let glob_t = it_mkProd_or_LetIn (mkSort s) arsign in
   let ((dep,_),univ) =
-    is_correct_arity env sigma kelim (c,p) indf (typP,glob_t) in
+    is_correct_arity env sigma kelim (c,pj) indf glob_t in
   (dep,univ)
 
 (* type_case_branches type un <p>Case c of ... end 
@@ -346,8 +346,9 @@ let find_case_dep_nparams env sigma (c,p) (IndFamily (mis,_) as indf) typP =
    attendus dans les branches du Case; lr est le type attendu du resultat
  *)
 
-let type_case_branches env sigma (IndType (indf,realargs)) pt p c =
-  let (dep,univ) = find_case_dep_nparams env sigma (c,p) indf pt in
+let type_case_branches env sigma (IndType (indf,realargs)) pj c =
+  let p = pj.uj_val in
+  let (dep,univ) = find_case_dep_nparams env sigma (c,pj) indf in
   let constructs = get_constructors indf in
   let lc = Array.map (build_branch_type env dep p) constructs in
   if dep then
@@ -355,17 +356,16 @@ let type_case_branches env sigma (IndType (indf,realargs)) pt p c =
   else 
     (lc, beta_applist (p,realargs), univ)
 
-let check_branches_message env sigma (c,ct) (explft,lft) = 
+let check_branches_message env sigma cj (explft,lft) = 
   let expn = Array.length explft and n = Array.length lft in
-  if n<>expn then error_number_branches CCI env c ct expn;
+  if n<>expn then error_number_branches CCI env cj expn;
   let univ = ref Constraint.empty in
   (for i = 0 to n-1 do
     try
       univ := Constraint.union !univ
         (conv_leq env sigma lft.(i) (explft.(i)))
     with NotConvertible ->
-      error_ill_formed_branch CCI env c i (nf_betaiota env sigma lft.(i))
-	(nf_betaiota env sigma explft.(i))
+      error_ill_formed_branch CCI env cj.uj_val i lft.(i) explft.(i)
   done;
   !univ)
 
@@ -373,14 +373,11 @@ let judge_of_case env sigma ci pj cj lfj =
   let lft = Array.map (fun j -> body_of_type j.uj_type) lfj in
   let indspec =
     try find_rectype env sigma (body_of_type cj.uj_type)
-    with Induc ->
-      error_case_not_inductive CCI env cj.uj_val (body_of_type cj.uj_type) in
+    with Induc -> error_case_not_inductive CCI env cj in
   let (bty,rslty,univ) =
-    type_case_branches env sigma indspec
-      (body_of_type pj.uj_type) pj.uj_val cj.uj_val in
+    type_case_branches env sigma indspec pj cj.uj_val in
   let kind = mysort_of_arity env sigma (body_of_type pj.uj_type) in
-  let univ' = check_branches_message env sigma
-    (cj.uj_val,body_of_type cj.uj_type) (bty,lft) in
+  let univ' = check_branches_message env sigma cj (bty,lft) in
   ({ uj_val  = mkMutCase (ci, pj.uj_val, cj.uj_val, Array.map j_val lfj);
      uj_type = rslty },
   Constraint.union univ univ')
diff --git a/kernel/typeops.mli b/kernel/typeops.mli
index 3008c87cb..e4464fd89 100644
--- a/kernel/typeops.mli
+++ b/kernel/typeops.mli
@@ -39,7 +39,7 @@ val judge_of_prop_contents : contents -> unsafe_judgment
 val judge_of_type : universe -> unsafe_judgment * constraints
 
 (*s Type of atomic terms. *)
-val relative : env -> 'a evar_map -> int -> unsafe_judgment
+val relative : env -> int -> unsafe_judgment
 
 val type_of_constant : env -> 'a evar_map -> constant -> types
 
@@ -85,11 +85,11 @@ val judge_of_case : env -> 'a evar_map -> case_info
     -> unsafe_judgment array -> unsafe_judgment * constraints
 
 val find_case_dep_nparams :
-  env -> 'a evar_map -> constr * constr -> inductive_family -> constr
+  env -> 'a evar_map -> constr * unsafe_judgment -> inductive_family
     -> bool * constraints
 
 val type_case_branches :
-  env -> 'a evar_map -> Inductive.inductive_type -> constr -> types
+  env -> 'a evar_map -> Inductive.inductive_type -> unsafe_judgment
     -> constr -> types array * types * constraints
 
 (*s Type of fixpoints and guard condition. *)
diff --git a/library/indrec.ml b/library/indrec.ml
index 36c9f884f..251656c60 100644
--- a/library/indrec.ml
+++ b/library/indrec.ml
@@ -470,11 +470,12 @@ let build_indrec env sigma mispec =
 (* To interpret the Match operator *)
 
 (* TODO: check that we can drop universe constraints ? *)
-let type_mutind_rec env sigma (IndType (indf,realargs) as ind) pt p c = 
+let type_mutind_rec env sigma (IndType (indf,realargs) as ind) pj c = 
+  let p = pj.uj_val in
   let (mispec,params) = dest_ind_family indf in
   let tyi = mis_index mispec in
   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_depPvec i = if i = tyi then Some(dep,p) else None in
     let depPvec = Array.init (mis_ntypes mispec) init_depPvec in
     let vargs = Array.of_list params in
@@ -486,13 +487,13 @@ let type_mutind_rec env sigma (IndType (indf,realargs) as ind) pt p c =
      if dep then applist(p,realargs@[c]) 
      else applist(p,realargs) )
   else 
-    let (p,ra,_) = type_case_branches env sigma ind pt p c in
+    let (p,ra,_) = type_case_branches env sigma ind pj c in
     (p,ra)
 
-let type_rec_branches recursive env sigma ind pt p c =
+let type_rec_branches recursive env sigma ind pj c =
   if recursive then 
-    type_mutind_rec env sigma ind pt p c
+    type_mutind_rec env sigma ind pj c
   else 
-    let (p,ra,_) = type_case_branches env sigma ind pt p c in
+    let (p,ra,_) = type_case_branches env sigma ind pj c in
     (p,ra)
 
diff --git a/library/indrec.mli b/library/indrec.mli
index 4f3cd5ee7..e50766348 100644
--- a/library/indrec.mli
+++ b/library/indrec.mli
@@ -39,7 +39,7 @@ val build_mutual_indrec :
 (* These are for old Case/Match typing *)
 
 val type_rec_branches : bool -> env -> 'c evar_map -> inductive_type
-  -> constr -> constr -> constr -> constr array * constr
+  -> unsafe_judgment -> constr -> constr array * constr
 val make_rec_branch_arg : 
   env -> 'a evar_map ->
     int * ('b * constr) option array * int ->
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. *)
 
diff --git a/proofs/clenv.ml b/proofs/clenv.ml
index 06a85319c..70f4f7080 100644
--- a/proofs/clenv.ml
+++ b/proofs/clenv.ml
@@ -96,8 +96,8 @@ let unify_0 mc wc m n =
   let env = w_env wc
   and sigma = w_Underlying wc in
   let rec unirec_rec ((metasubst,evarsubst) as substn) m n =
-    let cM = whd_ise1 sigma m
-    and cN = whd_ise1 sigma n in 
+    let cM = Evarutil.whd_castappevar sigma m
+    and cN = Evarutil.whd_castappevar sigma n in 
     try 
       match (kind_of_term cM,kind_of_term cN) with
 	| IsCast (c,_), _ -> unirec_rec substn c cN
diff --git a/proofs/evar_refiner.ml b/proofs/evar_refiner.ml
index 957605dfd..f99608691 100644
--- a/proofs/evar_refiner.ml
+++ b/proofs/evar_refiner.ml
@@ -119,7 +119,7 @@ let w_Focusing sp wt =
 let w_Focus sp wc = ids_mod (extract_decl sp) wc
 
 let w_Underlying wc = (ts_it (ids_it wc)).decls
-let w_whd wc c      = whd_castappevar (w_Underlying wc) c
+let w_whd wc c      = Evarutil.whd_castappevar (w_Underlying wc) c
 let w_type_of wc c  = ctxt_type_of (ids_it wc) c
 let w_env     wc    = get_env (ids_it wc)
 let w_hyps    wc    = named_context (get_env (ids_it wc))
diff --git a/proofs/logic.ml b/proofs/logic.ml
index 663b21a8a..3f22a6f8b 100644
--- a/proofs/logic.ml
+++ b/proofs/logic.ml
@@ -95,7 +95,7 @@ let rec mk_refgoals sigma goal goalacc conclty trm =
 	if occur_meta conclty then
           raise (RefinerError (OccurMetaGoal conclty));
 	let ctxt = out_some goal.evar_info in 
-	(mk_goal ctxt hyps (nf_betaiota env sigma conclty))::goalacc, conclty
+	(mk_goal ctxt hyps (nf_betaiota conclty))::goalacc, conclty
 
     | IsCast (t,ty) ->
 	let _ = type_of env sigma ty in
@@ -135,7 +135,7 @@ and mk_hdgoals sigma goal goalacc trm =
     | IsCast (c,ty) when isMeta c ->
 	let _ = type_of env sigma ty in
 	let ctxt = out_some goal.evar_info in  
-	(mk_goal ctxt hyps (nf_betaiota env sigma ty))::goalacc,ty
+	(mk_goal ctxt hyps (nf_betaiota ty))::goalacc,ty
 
     | IsApp (f,l) ->
 	let (acc',hdty) = mk_hdgoals sigma goal goalacc f in
@@ -168,10 +168,12 @@ and mk_casegoals sigma goal goalacc p c =
   let env = evar_env goal in
   let (acc',ct) = mk_hdgoals sigma goal goalacc c in 
   let (acc'',pt) = mk_hdgoals sigma goal acc' p in
+  let pj = {uj_val=p; uj_type=pt} in 
   let indspec =
     try find_rectype env sigma ct
     with Induc -> anomaly "mk_casegoals" in
-  let (lbrty,conclty,_) = type_case_branches env sigma indspec pt p c in
+  let (lbrty,conclty,_) =
+    type_case_branches env sigma indspec pj c in
   (acc'',lbrty,conclty)
 
 
diff --git a/proofs/refiner.ml b/proofs/refiner.ml
index 8e358adea..cfb5e64f9 100644
--- a/proofs/refiner.ml
+++ b/proofs/refiner.ml
@@ -49,7 +49,7 @@ let rec and_status = function
    (i.e. when the sigma of the proof tree changes) *)
 
 let norm_goal sigma gl =
-  let red_fun = nf_ise1 sigma in
+  let red_fun = Evarutil.nf_evar sigma in
   let ncl = red_fun gl.evar_concl in
   { evar_concl = ncl;
     evar_hyps = map_named_context red_fun gl.evar_hyps;
diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml
index b3ad1225e..b68196ff3 100644
--- a/proofs/tacmach.ml
+++ b/proofs/tacmach.ml
@@ -98,7 +98,7 @@ let pf_whd_betadeltaiota_stack   = pf_reduce whd_betadeltaiota_stack
 let pf_hnf_constr                = pf_reduce hnf_constr
 let pf_red_product               = pf_reduce red_product
 let pf_nf                        = pf_reduce nf
-let pf_nf_betaiota               = pf_reduce nf_betaiota
+let pf_nf_betaiota               = pf_reduce (fun _ _ -> nf_betaiota)
 let pf_compute                   = pf_reduce compute
 let pf_unfoldn ubinds            = pf_reduce (unfoldn ubinds)
 let pf_type_of                   = pf_reduce type_of
diff --git a/scripts/coqmktop.ml b/scripts/coqmktop.ml
index ee3acb5f4..8e80e6dcb 100644
--- a/scripts/coqmktop.ml
+++ b/scripts/coqmktop.ml
@@ -238,9 +238,11 @@ let declare_loading_string () =
     "Mltop.set Mltop.WithoutTop;;\n"
   else
     "let ppf = Format.std_formatter;;
-     Mltop.set (Mltop.WithTop {Mltop.load_obj=Topdirs.dir_load ppf;
-                               Mltop.use_file=Topdirs.dir_use ppf;
-                               Mltop.add_dir=Topdirs.dir_directory});;\n"
+     Mltop.set (Mltop.WithTop
+       {Mltop.load_obj=Topdirs.dir_load ppf;
+        Mltop.use_file=Topdirs.dir_use ppf;
+        Mltop.add_dir=Topdirs.dir_directory;
+        Mltop.ml_loop=(fun () -> Toploop.loop ppf) });;\n"
 
 (* create a temporary main file to link *)
 let create_tmp_main_file modules =
@@ -258,9 +260,6 @@ let create_tmp_main_file modules =
       output_string oc "Cmd_searchisos_line.start();;\n"
     else 
       output_string oc "Coqtop.start();;\n";
-    (* Start the Ocaml toplevel if it exists *)
-    if !top then
-      output_string oc "Printexc.catch Toploop.loop ppf; exit 1;;\n";
     close_out oc;
     main_name
   with e -> 
diff --git a/tactics/eauto.ml b/tactics/eauto.ml
index f86262b5c..38bb22342 100644
--- a/tactics/eauto.ml
+++ b/tactics/eauto.ml
@@ -103,17 +103,9 @@ let instantiate_tac = function
       (fun gl -> instantiate n c gl)
   | _ -> invalid_arg "Instantiate called with bad arguments"
 
-let whd_evar env sigma c = match kind_of_term c with
-  | IsEvar (n, cl) when Evd.in_dom sigma n & Evd.is_defined sigma n ->
-        Instantiate.existential_value sigma (n,cl)
-  | _ -> c
-
 let normEvars gl =
   let sigma = project gl in
-  let env = pf_env gl in
-  let nf_evar = strong whd_evar
-  and simplify = nf_betaiota in 
-  convert_concl (nf_evar env sigma (simplify env sigma (pf_concl gl))) gl
+  convert_concl (nf_betaiota (Evarutil.nf_evar sigma (pf_concl gl))) gl
 
 let vernac_prolog =
   let uncom = function
diff --git a/tactics/wcclausenv.ml b/tactics/wcclausenv.ml
index 3215cf017..63504956c 100644
--- a/tactics/wcclausenv.ml
+++ b/tactics/wcclausenv.ml
@@ -91,8 +91,8 @@ let clenv_constrain_with_bindings bl clause =
 	  in
 	  let env = Global.env () in
 	  let sigma = Evd.empty in
-	  let k_typ = nf_betaiota env sigma (clenv_instance_type clause k) in
-	  let c_typ = nf_betaiota env sigma (w_type_of clause.hook c) in 
+	  let k_typ = nf_betaiota (clenv_instance_type clause k) in
+	  let c_typ = nf_betaiota (w_type_of clause.hook c) in 
 	  matchrec (clenv_assign k c (clenv_unify k_typ c_typ clause)) t
     in 
     matchrec clause bl
diff --git a/toplevel/coqinit.ml b/toplevel/coqinit.ml
index 01dec915a..80c81d243 100644
--- a/toplevel/coqinit.ml
+++ b/toplevel/coqinit.ml
@@ -91,3 +91,16 @@ let init_library_roots () =
   List.iter
     (fun (_,alias,_) -> Nametab.push_library_root (List.hd alias)) !includes;
   includes := []
+
+(* Initialises the Ocaml toplevel before launching it, so that it can
+   find the "include" file in the *source* directory *)
+let init_ocaml_path () =
+(* We only assume that the variable COQTOP is set *)
+  let coqtop = getenv_else "COQTOP" Coq_config.coqtop in
+  let add_subdir dl = 
+    Mltop.add_ml_dir (List.fold_left Filename.concat coqtop dl) 
+  in
+  List.iter add_subdir
+    [ [ "config" ]; [ "dev" ]; [ "lib" ]; [ "kernel" ]; [ "library" ]; 
+      [ "pretyping" ]; [ "parsing" ]; [ "proofs" ]; [ "tactics" ];
+      [ "toplevel" ] ]
diff --git a/toplevel/coqinit.mli b/toplevel/coqinit.mli
index 81a83eeea..af2c27be9 100644
--- a/toplevel/coqinit.mli
+++ b/toplevel/coqinit.mli
@@ -23,3 +23,5 @@ val push_rec_include : string * Names.dir_path -> unit
 
 val init_load_path : unit -> unit
 val init_library_roots : unit -> unit
+
+val init_ocaml_path : unit -> unit
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index 27bb17d85..befe4cf43 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -213,6 +213,10 @@ let start () =
       exit 1
   end;
   if !batch_mode then (flush_all(); Profile.print_profile ();exit 0);
-  Toplevel.loop()
+  Toplevel.loop();
+(* Initialise and launch the Ocaml toplevel *)
+  Coqinit.init_ocaml_path();
+  Mltop.ocaml_toploop();
+  exit 1
 
 (* [Coqtop.start] will be called by the code produced by coqmktop *)
diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml
index 4daec6d52..e9194d8a8 100644
--- a/toplevel/himsg.ml
+++ b/toplevel/himsg.ml
@@ -63,12 +63,12 @@ let msg_bad_elimination ctx k = function
   | None -> 
       [<>]
 
-let explain_elim_arity k ctx ind aritylst c p pt okinds = 
+let explain_elim_arity k ctx ind aritylst c pj okinds = 
   let pi = pr_inductive ctx ind in
   let ppar = prlist_with_sep pr_coma (prterm_env ctx) aritylst in
   let pc = prterm_env ctx c in
-  let pp = prterm_env ctx p in
-  let ppt = prterm_env ctx pt in
+  let pp = prterm_env ctx pj.uj_val in
+  let ppt = prterm_env ctx pj.uj_type in
   [< 'sTR "Incorrect elimination of"; 'bRK(1,1); pc; 'sPC;
      'sTR "in the inductive type"; 'bRK(1,1); pi; 'fNL;
      'sTR "The elimination predicate"; 'bRK(1,1); pp; 'sPC;
@@ -76,16 +76,16 @@ let explain_elim_arity k ctx ind aritylst c p pt okinds =
      'sTR "It should be one of :"; 'bRK(1,1) ; hOV 0 ppar; 'fNL;
      msg_bad_elimination ctx k okinds >]
 
-let explain_case_not_inductive k ctx c ct =
-  let pc = prterm_env ctx c in
-  let pct = prterm_env ctx ct in
+let explain_case_not_inductive k ctx cj =
+  let pc = prterm_env ctx cj.uj_val in
+  let pct = prterm_env ctx cj.uj_type in
   [< 'sTR "In Cases expression, the matched term"; 'bRK(1,1); pc; 'sPC; 
      'sTR "has type"; 'bRK(1,1); pct; 'sPC; 
      'sTR "which is not a (co-)inductive type" >]
   
-let explain_number_branches k ctx c ct expn =
-  let pc = prterm_env ctx c in
-  let pct = prterm_env ctx ct in
+let explain_number_branches k ctx cj expn =
+  let pc = prterm_env ctx cj.uj_val in
+  let pct = prterm_env ctx cj.uj_type in
   [< 'sTR "Cases on term"; 'bRK(1,1); pc; 'sPC ;
      'sTR "of type"; 'bRK(1,1); pct; 'sPC;
      'sTR "expects ";  'iNT expn; 'sTR " branches" >]
@@ -159,20 +159,21 @@ let explain_cant_apply_not_functional k ctx rator randl =
      'sTR"The expression"; 'bRK(1,1); pr; 'sPC;
      'sTR"of type"; 'bRK(1,1); prt; 'sPC ;
      'sTR("cannot be applied to the "^term_string); 'fNL; 
-     'sTR" "; v 0 appl; 'fNL >]
+     'sTR" "; v 0 appl >]
 
 let explain_unexpected_type k ctx actual_type expected_type =
   let ctx = make_all_name_different ctx in
   let pract = prterm_env ctx actual_type in
   let prexp = prterm_env ctx expected_type in
   [< 'sTR"This type is"; 'sPC; pract; 'sPC; 'sTR "but is expected to be";
-     'sPC; prexp; 'fNL >]
+     'sPC; prexp >]
 
 let explain_not_product k ctx c =
   let ctx = make_all_name_different ctx in
   let pr = prterm_env ctx c in
-  [< 'sTR"The type of this term is expected to be a product but it is";
-     'bRK(1,1); pr; 'fNL >]
+  [< 'sTR"The type of this term is a product,"; 'sPC;
+     'sTR"but it is casted with type";
+     'bRK(1,1); pr >]
 
 (* TODO: use the names *)
 (* (co)fixpoints *)
@@ -248,15 +249,6 @@ let explain_cant_find_case_type k ctx c =
   let pe = prterm_env ctx c in
   hOV 3 [<'sTR "Cannot infer type of whole Case expression on"; 'wS 1; pe >]
 
-(***
-let explain_cant_find_case_type_loc loc k ctx c =
-  let pe = prterm_env ctx c in
-  user_err_loc
-    (loc,"pretype",
-     hOV 3 [<'sTR "Cannot infer type of whole Case expression on"; 
-	     'wS 1; pe >])
-***)
-
 let explain_occur_check k ctx ev rhs =
   let id = "?" ^ string_of_int ev in
   let pt = prterm_env ctx rhs in
@@ -285,12 +277,12 @@ let explain_type_error k ctx = function
       explain_bad_assumption k ctx c
   | ReferenceVariables id -> 
       explain_reference_variables id
-  | ElimArity (ind, aritylst, c, p, pt, okinds) ->
-      explain_elim_arity k ctx ind aritylst c p pt okinds 
-  | CaseNotInductive (c, ct) -> 
-      explain_case_not_inductive k ctx c ct
-  | NumberBranches (c, ct, n) -> 
-      explain_number_branches k ctx c ct n
+  | ElimArity (ind, aritylst, c, pj, okinds) ->
+      explain_elim_arity k ctx ind aritylst c pj okinds 
+  | CaseNotInductive cj -> 
+      explain_case_not_inductive k ctx cj
+  | NumberBranches (cj, n) -> 
+      explain_number_branches k ctx cj n
   | IllFormedBranch (c, i, actty, expty) -> 
       explain_ill_formed_branch k ctx c i actty expty 
   | Generalization (nvar, c) ->
@@ -310,7 +302,7 @@ let explain_type_error k ctx = function
       explain_not_inductive k ctx c
 *)
 let explain_pretype_error ctx = function
-  | MlCase mes ->
+  | MlCase (mes,_,_) ->
       explain_ml_case CCI ctx mes
   | CantFindCaseType c ->
       explain_cant_find_case_type CCI ctx c
diff --git a/toplevel/mltop.ml4 b/toplevel/mltop.ml4
index 531e52752..0499eff83 100644
--- a/toplevel/mltop.ml4
+++ b/toplevel/mltop.ml4
@@ -51,7 +51,8 @@ let keep_copy_mlpath s =
 type toplevel = { 
   load_obj : string -> unit;
   use_file : string -> unit;
-  add_dir  : string -> unit }
+  add_dir  : string -> unit;
+  ml_loop  : unit -> unit }
 
 (* Determines the behaviour of Coq with respect to ML files (compiled 
    or not) *)
@@ -82,6 +83,16 @@ let enable_load () =
     | WithTop _ | WithoutTop -> true
     |_ -> false
 
+(* Runs the toplevel loop of Ocaml *)
+let ocaml_toploop () =
+  match !load with
+    | WithTop t -> Printexc.catch t.ml_loop ()
+    | _ -> ()
+(*
+        errorlabstrm "Mltop.ocaml_toploop"
+          [< 'sTR"Cannot access the ML toplevel" >]
+*)
+
 (* Dynamic loading of .cmo *)
 let dir_ml_load s = 
   match !load with
diff --git a/toplevel/mltop.mli b/toplevel/mltop.mli
index 17c3f192f..8e493ad02 100644
--- a/toplevel/mltop.mli
+++ b/toplevel/mltop.mli
@@ -10,10 +10,11 @@
 
 (* If there is a toplevel under Coq, it is described by the following 
    record. *)
-type toplevel = {
+type toplevel = { 
   load_obj : string -> unit;
   use_file : string -> unit;
-  add_dir : string -> unit }
+  add_dir  : string -> unit;
+  ml_loop  : unit -> unit }
 
 (* Determines the behaviour of Coq with respect to ML files (compiled 
    or not) *) 
@@ -35,6 +36,9 @@ val is_ocaml_top : unit -> bool
 (*Tests if we can load ML files*)
 val enable_load : unit -> bool
 
+(*Starts the Ocaml toplevel loop *)
+val ocaml_toploop : unit -> unit
+
 (*Dynamic loading of .cmo*)
 val dir_ml_load : string -> unit
 
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index fbc9dc152..8d684633b 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -14,22 +14,16 @@ open Declarations
 open Pp
 open Util
 open Options
-open Stamps
 open System
 open Names
 open Term
-open Evd
-open Reduction
 open Pfedit
 open Tacmach
 open Proof_trees
 open Proof_type
 open Tacred
-open Library
-open Libobject
 open Environ
 open Vernacinterp
-open Declare
 open Coqast
 open Ast
 open Astterm
@@ -39,8 +33,7 @@ open Tacinterp
 open Tactic_debug
 open Command
 open Goptions
-open Mltop
-open Nametab
+open Declare
 
 (* Dans join_binders, s'il y a un "?", on perd l'info qu'il est partagé *)
 let join_binders binders = 
@@ -121,7 +114,7 @@ let locate_qualid loc qid =
     let _ = Syntax_def.locate_syntactic_definition qid in
     error
       ("Unexpected reference to a syntactic definition: "
-       ^(string_of_qualid qid))
+       ^(Nametab.string_of_qualid qid))
   with Not_found ->
     Nametab.error_global_not_found_loc loc qid
 
@@ -130,7 +123,8 @@ let global = locate_qualid
 
 let locate_file f =
   try
-    let _,file = System.where_in_path (get_load_path()) f in
+    let _,file =
+      System.where_in_path (Library.get_load_path()) f in
     mSG [< 'sTR file; 'fNL >]
   with Not_found -> 
     mSG (hOV 0 [< 'sTR"Can't find file"; 'sPC; 'sTR f; 'sPC;
@@ -147,13 +141,13 @@ let print_located_qualid qid =
       [< 'sTR (string_of_path (Syntax_def.locate_syntactic_definition qid));
 	 'fNL >]
   with Not_found ->
-    error ((string_of_qualid qid) ^ " not a defined object")
+    error ((Nametab.string_of_qualid qid) ^ " not a defined object")
 
 let print_path_entry s =
   [< 'sTR s.directory; 'tBRK (0,2); 'sTR (string_of_dirpath s.coq_dirpath) >]
 
 let print_loadpath () =
-  let l = get_load_path () in
+  let l = Library.get_load_path () in
   mSGNL (Pp.t [< 'sTR "Physical path:                                 ";
 		 'tAB; 'sTR "Logical Path:"; 'fNL; 
 		 prlist_with_sep pr_fnl print_path_entry l >])
@@ -193,29 +187,29 @@ let _ =
   add "ADDPATH"
     (function 
        | [VARG_STRING dir] ->
-	   (fun () -> add_path dir [Nametab.default_root])
+	   (fun () -> Mltop.add_path dir [Nametab.default_root])
        | [VARG_STRING dir ; VARG_QUALID alias] ->
            let aliasdir,aliasname = Nametab.repr_qualid alias in
-	    (fun () -> add_path dir (aliasdir@[string_of_id aliasname]))
+	    (fun () -> Mltop.add_path dir (aliasdir@[string_of_id aliasname]))
        | _ -> bad_vernac_args "ADDPATH")
 
 (* For compatibility *)
 let _ =
   add "DELPATH"
     (function 
-       | [VARG_STRING dir] -> (fun () -> remove_path dir)
+       | [VARG_STRING dir] -> (fun () -> Library.remove_path dir)
        | _ -> bad_vernac_args "DELPATH")
 
 let _ = 
   add "RECADDPATH"
     (function 
        | [VARG_STRING dir] ->
-	   (fun () -> add_rec_path dir [Nametab.default_root])
+	   (fun () -> Mltop.add_rec_path dir [Nametab.default_root])
        | [VARG_STRING dir ; VARG_QUALID alias] ->
            let aliasdir,aliasname = Nametab.repr_qualid alias in
 	    (fun () ->
 	       let alias = aliasdir@[string_of_id aliasname] in
-	       add_rec_path dir alias;
+	       Mltop.add_rec_path dir alias;
 	       Nametab.push_library_root (List.hd alias))
        | _ -> bad_vernac_args "RECADDPATH")
 
@@ -395,7 +389,7 @@ let _ =
        | [VARG_CONSTR com] ->
 	   (fun () ->
               if not (refining()) then begin
-              	start_proof_com None NeverDischarge com;
+              	start_proof_com None Declare.NeverDischarge com;
 		if_verbose show_open_subgoals ()
               end else 
 		error "repeated Goal not permitted in refining mode")
@@ -553,11 +547,11 @@ let _ =
 		   let coe = coercion_of_qualid dummy_loc qid in
 	           if Classops.is_coercion_visible coe then
 		     message
-		       ("Printing of coercion "^(string_of_qualid qid)^
+		       ("Printing of coercion "^(Nametab.string_of_qualid qid)^
 			" is set")
 		   else 
 		     message 
-		       ("Printing of coercion "^(string_of_qualid qid)^
+		       ("Printing of coercion "^(Nametab.string_of_qualid qid)^
 			" is unset"))
 		ql))
     
@@ -714,7 +708,7 @@ let _ =
 			 (fun (mv,ty) -> 
 			    [< 'iNT mv ; 'sTR" -> " ; prtype ty ; 'fNL >])
 			 meta_types;
-		       'sTR"Proof: " ; prterm (nf_ise1 evc pfterm) >])
+		       'sTR"Proof: " ; prterm (Evarutil.nf_evar evc pfterm) >])
        | _ -> bad_vernac_args "ShowProof")
 
 let _ =
@@ -1026,7 +1020,7 @@ let extract_qualid = function
   | VARG_QUALID qid ->
       (try wd_of_sp (fst (Nametab.locate_module qid))
        with Not_found -> 
-	 error ("Module/section "^(string_of_qualid qid)^" not found"))
+	 error ("Module/section "^(Nametab.string_of_qualid qid)^" not found"))
   | _ -> bad_vernac_args "extract_qualid"
 
 let inside_outside = function
@@ -1349,11 +1343,12 @@ let _ =
 	   fun () -> 
 	     let ref = locate_qualid dummy_loc qid in
 	     Class.try_add_new_class ref stre;
-             if_verbose message ((string_of_qualid qid) ^ " is now a class")
+             if_verbose message
+               ((Nametab.string_of_qualid qid) ^ " is now a class")
        | _ -> bad_vernac_args "CLASS")
 
 let cl_of_qualid qid =
-  match repr_qualid qid with
+  match Nametab.repr_qualid qid with
     | [], id when string_of_id id = "FUNCLASS" -> Classops.CL_FUN
     | [], id when string_of_id id = "SORTCLASS" -> Classops.CL_SORT
     | _ -> Class.class_of_ref (locate_qualid dummy_loc qid)	
@@ -1373,7 +1368,7 @@ let _ =
 	   let target = cl_of_qualid qidt in
 	   let source = cl_of_qualid qids in
 	   fun () ->
-	     if isid then match repr_qualid qid with
+	     if isid then match Nametab.repr_qualid qid with
 	       | [], id ->
 		   Class.try_add_new_identity_coercion id stre source target
 	       | _ -> bad_vernac_args "COERCION"
@@ -1381,7 +1376,8 @@ let _ =
 	       let ref = locate_qualid dummy_loc qid in
 	       Class.try_add_new_coercion_with_target ref stre source target;
 	       if_verbose
-		 message ((string_of_qualid qid) ^ " is now a coercion")
+		 message
+                 ((Nametab.string_of_qualid qid) ^ " is now a coercion")
        | _ -> bad_vernac_args "COERCION")
 
 let _ =
@@ -1672,7 +1668,7 @@ let _ =
             if (string_of_id t) = "Tables" then 
 	      print_tables ()
 	    else 
-	      mSG(print_name (make_qualid [] t)))
+	      mSG(print_name (Nametab.make_qualid [] t)))
      | _ -> bad_vernac_args "TableField")
 
 
@@ -1736,26 +1732,26 @@ let _ = vinterp_add "DeclareMLModule"
 		    | (VARG_STRING s) -> s 
 		    | _ -> anomaly "DeclareMLModule : not a string") l
 	     in
-    	     fun () -> declare_ml_modules sl)
+    	     fun () -> Mltop.declare_ml_modules sl)
 	  
 let _ = vinterp_add "AddMLPath"
 	  (function 
 	     | [VARG_STRING s] ->
-		 (fun () -> add_ml_dir (glob s))
+		 (fun () -> Mltop.add_ml_dir (glob s))
 	     | _ -> anomaly "AddMLPath : not a string")
 
 let _ = vinterp_add "RecAddMLPath"
 	  (function 
 	     | [VARG_STRING s] ->
-		 (fun () -> add_rec_ml_dir (glob s))
+		 (fun () -> Mltop.add_rec_ml_dir (glob s))
 	     | _ -> anomaly "RecAddMLPath : not a string")
 
 let _ = vinterp_add "PrintMLPath"
 	  (function 
-	     | [] -> (fun () -> print_ml_path ())
+	     | [] -> (fun () -> Mltop.print_ml_path ())
 	     | _ -> anomaly "PrintMLPath : does not expect any argument")
 
 let _ = vinterp_add "PrintMLModules"
 	  (function 
-	     | [] -> (fun () -> print_ml_modules ())
+	     | [] -> (fun () -> Mltop.print_ml_modules ())
 	     | _ -> anomaly "PrintMLModules : does not expect an argument")