pushed evar reduction in kernel

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

13 files changed, 189 insertions, 188 deletions

diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index 00df4c87a2..dcedfa51d5 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -981,7 +981,8 @@ let specialize_predicate newtomatchs (names,(depna,_)) cs tms ccl =
   let copti = if depna<>Anonymous then Some (build_dependent_constructor cs) else None in
   (* The substituends argsi, copti are all defined in gamma, x1...xn *)
   (* We need _parallel_ bindings to get gamma, x1...xn, tms |- ccl'' *)
-  let ccl'' = whd_betaiota (subst_predicate (argsi, copti) ccl' tms) in
+  let ccl'' =
+    whd_betaiota Evd.empty (subst_predicate (argsi, copti) ccl' tms) in
   (* We adjust ccl st: gamma, x1..xn, x1..xn, tms |- ccl'' *)
   let ccl''' = liftn_predicate n (n+1) ccl'' tms in
   (* We finally get gamma,x1..xn |- [X1,x1:=R1,x1]..[Xn,xn:=Rn,xn]pred'''*)
@@ -989,7 +990,8 @@ let specialize_predicate newtomatchs (names,(depna,_)) cs tms ccl =
 
 let find_predicate loc env evdref p current (IndType (indf,realargs)) dep tms =
   let pred= abstract_predicate env (evars_of !evdref) indf current dep tms p in
-  (pred, whd_betaiota (applist (pred, realargs@[current])), new_Type ())
+  (pred, whd_betaiota (evars_of !evdref)
+           (applist (pred, realargs@[current])), new_Type ())
 
 let adjust_predicate_from_tomatch ((_,oldtyp),_,(nadep,_)) typ pb =
   match typ, oldtyp with
@@ -1211,7 +1213,7 @@ and match_current pb tomatch =
 	    find_predicate pb.caseloc pb.env pb.evdref 
 	      pb.pred current indt (names,dep) pb.tomatch in
 	  let ci = make_case_info pb.env mind pb.casestyle in
-	  let case = mkCase (ci,nf_betaiota pred,current,brvals) in
+	  let case = mkCase (ci,nf_betaiota Evd.empty pred,current,brvals) in
 	  let inst = List.map mkRel deps in
 	  { uj_val = applist (case, inst);
 	    uj_type = substl inst typ }
@@ -1454,8 +1456,8 @@ let adjust_to_extended_env_and_remove_deps env extenv subst t =
 *)
 
 let abstract_tycon loc env evdref subst _tycon extenv t =
-  let t = nf_betaiota t in (* it helps in some cases to remove K-redex... *)
   let sigma = evars_of !evdref in
+  let t = nf_betaiota sigma t in (* it helps in some cases to remove K-redex *)
   let subst0,t0 = adjust_to_extended_env_and_remove_deps env extenv subst t in
   (* We traverse the type T of the original problem Xi looking for subterms
      that match the non-constructor part of the constraints (this part
diff --git a/pretyping/cbv.ml b/pretyping/cbv.ml
index ea7f6f065c..1794382523 100644
--- a/pretyping/cbv.ml
+++ b/pretyping/cbv.ml
@@ -218,6 +218,11 @@ let rec norm_head info env t stack =
 		   cbv_norm_term info env' c) in
 	(VAL(0,normt), stack) (* Considérer une coupure commutative ? *)
 
+  | Evar ev ->
+      (match evar_value info ev with
+          Some c -> norm_head info env c stack
+        | None -> (VAL(0, t), stack))
+
   (* non-neutral cases *)
   | Lambda _ ->
       let ctxt,b = decompose_lam t in
@@ -227,7 +232,7 @@ let rec norm_head info env t stack =
   | Construct c -> (CONSTR(c, [||]), stack)
 
   (* neutral cases *)
-  | (Sort _ | Meta _ | Ind _|Evar _) -> (VAL(0, t), stack)
+  | (Sort _ | Meta _ | Ind _) -> (VAL(0, t), stack)
   | Prod (x,t,c) -> 
       (VAL(0, mkProd (x, cbv_norm_term info env t,
 		      cbv_norm_term info (subs_lift env) c)),
@@ -353,8 +358,9 @@ let cbv_norm infos constr =
 type cbv_infos = cbv_value infos
 
 (* constant bodies are normalized at the first expansion *)
-let create_cbv_infos flgs env =
+let create_cbv_infos flgs env sigma =
   create
     (fun old_info c -> cbv_stack_term old_info TOP (ESID 0) c)
     flgs
     env
+    (Reductionops.safe_evar_value sigma)
diff --git a/pretyping/cbv.mli b/pretyping/cbv.mli
index 21b65a57e9..461115a568 100644
--- a/pretyping/cbv.mli
+++ b/pretyping/cbv.mli
@@ -22,7 +22,7 @@ open Esubst
 (* Entry point for cbv normalization of a constr *)
 type cbv_infos
 
-val create_cbv_infos : RedFlags.reds -> env -> cbv_infos
+val create_cbv_infos : RedFlags.reds -> env -> Evd.evar_map -> cbv_infos
 val cbv_norm         : cbv_infos -> constr -> constr
 
 (************************************************************************)
diff --git a/pretyping/classops.ml b/pretyping/classops.ml
index 548ca7596f..b0554540af 100644
--- a/pretyping/classops.ml
+++ b/pretyping/classops.ml
@@ -143,7 +143,7 @@ let coercion_params coe_info = coe_info.coe_param
 (* find_class_type : env -> evar_map -> constr -> cl_typ * int *)
 
 let find_class_type env sigma t =
-  let t', args = Reductionops.whd_betaiotazetaevar_stack env sigma t in
+  let t', args = Reductionops.whd_betaiotazeta_stack sigma t in
   match kind_of_term t' with
     | Var id -> CL_SECVAR id, args
     | Const sp -> CL_CONST sp, args
diff --git a/pretyping/clenv.ml b/pretyping/clenv.ml
index 732ff1e69b..24f3b77260 100644
--- a/pretyping/clenv.ml
+++ b/pretyping/clenv.ml
@@ -254,7 +254,7 @@ let clenv_unify_meta_types ?(flags=default_unify_flags) clenv =
   { clenv with evd = w_unify_meta_types ~flags:flags clenv.env clenv.evd }
 
 let clenv_unique_resolver allow_K ?(flags=default_unify_flags) clenv gl =
-  if isMeta (fst (whd_stack clenv.templtyp.rebus)) then
+  if isMeta (fst (whd_stack (evars_of clenv.evd) clenv.templtyp.rebus)) then
     clenv_unify allow_K CUMUL ~flags:flags (clenv_type clenv) (pf_concl gl)
       (clenv_unify_meta_types ~flags:flags clenv)
   else
@@ -402,7 +402,7 @@ let error_already_defined b =
           (str "Position " ++ int n ++ str" already defined.")
 
 let clenv_unify_binding_type clenv c t u =
-  if isMeta (fst (whd_stack u)) then
+  if isMeta (fst (whd_stack (evars_of clenv.evd) u)) then
     (* Not enough information to know if some subtyping is needed *)
     CoerceToType, clenv, c
   else
@@ -416,7 +416,7 @@ let clenv_unify_binding_type clenv c t u =
 let clenv_assign_binding clenv k (sigma,c) =
   let k_typ = clenv_hnf_constr clenv (clenv_meta_type clenv k) in
   let clenv' = { clenv with evd = evar_merge clenv.evd sigma} in
-  let c_typ = nf_betaiota (clenv_get_type_of clenv' c) in
+  let c_typ = nf_betaiota (evars_of clenv'.evd) (clenv_get_type_of clenv' c) in
   let status,clenv'',c = clenv_unify_binding_type clenv' c c_typ k_typ in
   { clenv'' with evd = meta_assign k (c,(UserGiven,status)) clenv''.evd }
 
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index 18cb9457df..aba6e2e198 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -62,7 +62,7 @@ let evar_apprec env evd stack c =
   in aux (c, append_stack_list stack empty_stack)
 
 let apprec_nohdbeta env evd c =
-  match kind_of_term (fst (Reductionops.whd_stack c)) with
+  match kind_of_term (fst (Reductionops.whd_stack (evars_of evd) c)) with
     | (Case _ | Fix _) -> applist (evar_apprec env evd [] c)
     | _ -> c
 
diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml
index 40599f4a35..fee8e29f50 100644
--- a/pretyping/evarutil.ml
+++ b/pretyping/evarutil.ml
@@ -122,7 +122,7 @@ let evars_to_metas sigma (emap, c) =
   let emap = nf_evars emap in
   let sigma',emap' = push_dependent_evars sigma emap in
   let change_exist evar =
-    let ty = nf_betaiota (nf_evar emap (existential_type emap evar)) in
+    let ty = nf_betaiota emap (existential_type emap evar) in
     let n = new_meta() in
     mkCast (mkMeta n, DEFAULTcast, ty) in
   let rec replace c =
@@ -909,7 +909,7 @@ let rec invert_definition env evd (evk,argsv as ev) rhs =
 	map_constr_with_full_binders (fun d (env,k) -> push_rel d env, k+1)
 	  imitate envk t in
 
-  let rhs = whd_beta rhs (* heuristic *) in
+  let rhs = whd_beta (evars_of evd) rhs (* heuristic *) in
   let body = imitate (env,0) rhs in
   (!evdref,body)
 
@@ -963,7 +963,7 @@ and evar_define env (evk,_ as ev) rhs evd =
  *)
 
 let has_undefined_evars evd t = 
-  try let _ = local_strong (whd_ise (evars_of evd)) t in false
+  try let _ = local_strong whd_ise (evars_of evd) t in false
   with Uninstantiated_evar _ -> true
 
 let is_ground_term evd t =
diff --git a/pretyping/indrec.ml b/pretyping/indrec.ml
index 689257c3b5..f8dab16cd7 100644
--- a/pretyping/indrec.ml
+++ b/pretyping/indrec.ml
@@ -229,7 +229,7 @@ let make_rec_branch_arg env sigma (nparrec,fvect,decF) f cstr recargs =
            | None ->
 	       lambda_name env
 		 (n,t,process_constr (push_rel d env) (i+1)
-		    (whd_beta (applist (lift 1 f, [(mkRel 1)])))
+		    (whd_beta Evd.empty (applist (lift 1 f, [(mkRel 1)])))
 		    (cprest,rest))
            | Some(_,f_0) -> 
 	       let nF = lift (i+1+decF) f_0 in
@@ -237,7 +237,7 @@ let make_rec_branch_arg env sigma (nparrec,fvect,decF) f cstr recargs =
 	       let arg = process_pos env' nF (lift 1 t) in 
                lambda_name env
 		 (n,t,process_constr env' (i+1)
-		    (whd_beta (applist (lift 1 f, [(mkRel 1); arg])))
+		    (whd_beta Evd.empty (applist (lift 1 f, [(mkRel 1); arg])))
 		    (cprest,rest)))
     | (n,Some c,t as d)::cprest, rest ->
 	mkLetIn
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index 9d99ed6d4c..8a40361d3d 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -114,31 +114,41 @@ type state = constr * constr stack
 
 type  contextual_reduction_function = env ->  evar_map -> constr -> constr
 type  reduction_function =  contextual_reduction_function
-type local_reduction_function = constr -> constr
+type local_reduction_function = evar_map -> constr -> constr
 
 type  contextual_stack_reduction_function = 
     env ->  evar_map -> constr -> constr * constr list
 type  stack_reduction_function =  contextual_stack_reduction_function
-type local_stack_reduction_function = constr -> constr * constr list
+type local_stack_reduction_function =
+    evar_map -> constr -> constr * constr list
 
 type  contextual_state_reduction_function = 
     env ->  evar_map -> state -> state
 type  state_reduction_function =  contextual_state_reduction_function
-type local_state_reduction_function = state -> state
+type local_state_reduction_function = evar_map -> state -> state
 
 (*************************************)
 (*** Reduction Functions Operators ***)
 (*************************************)
 
-let rec whd_app_state (x, stack as s) =
+let safe_evar_value sigma ev =
+  try Some (Evd.existential_value sigma ev)
+  with NotInstantiatedEvar | Not_found -> None
+
+let rec whd_app_state sigma (x, stack as s) =
   match kind_of_term x with
-    | App (f,cl) -> whd_app_state (f, append_stack cl stack)
-    | Cast (c,_,_)  -> whd_app_state (c, stack)
+    | App (f,cl) -> whd_app_state sigma (f, append_stack cl stack)
+    | Cast (c,_,_)  -> whd_app_state sigma (c, stack)
+    | Evar ev ->
+        (match safe_evar_value sigma ev with
+            Some c -> whd_app_state sigma (c,stack)
+          | _ -> s)
     | _             -> s
 
 let appterm_of_stack (f,s) = (f,list_of_stack s)
 
-let whd_stack x = appterm_of_stack (whd_app_state (x, empty_stack))
+let whd_stack sigma x =
+  appterm_of_stack (whd_app_state sigma (x, empty_stack))
 let whd_castapp_stack = whd_stack
 
 let stack_reduction_of_reduction red_fun env sigma s =
@@ -150,14 +160,14 @@ let strong whdfun env sigma t =
     map_constr_with_full_binders push_rel strongrec env (whdfun env sigma t) in
   strongrec env t
 
-let local_strong whdfun = 
-  let rec strongrec t = map_constr strongrec (whdfun t) in
+let local_strong whdfun sigma = 
+  let rec strongrec t = map_constr strongrec (whdfun sigma t) in
   strongrec
 
-let rec strong_prodspine redfun c = 
-  let x = redfun c in
+let rec strong_prodspine redfun sigma c = 
+  let x = redfun sigma c in
   match kind_of_term x with
-    | Prod (na,a,b) -> mkProd (na,a,strong_prodspine redfun b)
+    | Prod (na,a,b) -> mkProd (na,a,strong_prodspine redfun sigma b)
     | _ -> x
 
 (*************************************)
@@ -171,7 +181,6 @@ module type RedFlagsSig = sig
   type flags
   type flag
   val fbeta : flag
-  val fevar : flag
   val fdelta : flag
   val feta : flag
   val fiota : flag
@@ -179,7 +188,6 @@ module type RedFlagsSig = sig
   val mkflags : flag list -> flags
   val red_beta : flags -> bool
   val red_delta : flags -> bool
-  val red_evar : flags -> bool
   val red_eta : flags -> bool
   val red_iota : flags -> bool
   val red_zeta : flags -> bool
@@ -191,14 +199,12 @@ module RedFlags = (struct
   type flags = int
   let fbeta = 1
   let fdelta = 2
-  let fevar = 4
   let feta = 8 
   let fiota = 16
   let fzeta = 32
   let mkflags = List.fold_left (lor) 0
   let red_beta f = f land fbeta <> 0
   let red_delta f = f land fdelta <> 0
-  let red_evar f = f land fevar <> 0
   let red_eta f = f land feta <> 0
   let red_iota f = f land fiota <> 0
   let red_zeta f = f land fzeta <> 0
@@ -209,20 +215,16 @@ open RedFlags
 (* Local *)
 let beta = mkflags [fbeta]
 let eta = mkflags [feta]
-let evar = mkflags [fevar]
-let betaevar = mkflags [fevar; fbeta]
 let betaiota = mkflags [fiota; fbeta]
 let betaiotazeta = mkflags [fiota; fbeta;fzeta]
-let betaiotazetaevar = mkflags [fiota; fbeta;fzeta;fevar]
 
 (* Contextual *)
-let delta = mkflags [fdelta;fevar]
-let betadelta = mkflags [fbeta;fdelta;fzeta;fevar]
-let betadeltaeta = mkflags [fbeta;fdelta;fzeta;fevar;feta]
-let betadeltaiota = mkflags [fbeta;fdelta;fzeta;fevar;fiota]
-let betadeltaiota_nolet = mkflags [fbeta;fdelta;fevar;fiota]
-let betadeltaiotaeta = mkflags [fbeta;fdelta;fzeta;fevar;fiota;feta]
-let betaiotaevar = mkflags [fbeta;fiota;fevar]
+let delta = mkflags [fdelta]
+let betadelta = mkflags [fbeta;fdelta;fzeta]
+let betadeltaeta = mkflags [fbeta;fdelta;fzeta;feta]
+let betadeltaiota = mkflags [fbeta;fdelta;fzeta;fiota]
+let betadeltaiota_nolet = mkflags [fbeta;fdelta;fiota]
+let betadeltaiotaeta = mkflags [fbeta;fdelta;fzeta;fiota;feta]
 let betaetalet = mkflags [fbeta;feta;fzeta]
 let betalet = mkflags [fbeta;fzeta]
 
@@ -283,11 +285,11 @@ let fix_recarg ((recindices,bodynum),_) stack =
 
 type fix_reduction_result = NotReducible | Reduced of state
 
-let reduce_fix whdfun fix stack =
+let reduce_fix whdfun sigma fix stack =
   match fix_recarg fix stack with
     | None -> NotReducible
     | Some (recargnum,recarg) ->
-        let (recarg'hd,_ as recarg') = whdfun (recarg, empty_stack) in
+        let (recarg'hd,_ as recarg') = whdfun sigma (recarg, empty_stack) in
         let stack' = stack_assign stack recargnum (app_stack recarg') in
 	(match kind_of_term recarg'hd with
            | Construct _ -> Reduced (contract_fix fix, stack')
@@ -313,8 +315,8 @@ let rec whd_state_gen flags env sigma =
 	  (match lookup_named id env with
 	     | (_,Some body,_) -> whrec (body, stack)
 	     | _ -> s)
-      | Evar ev when red_evar flags ->
-	  (match existential_opt_value sigma ev with
+      | Evar ev ->
+	  (match safe_evar_value sigma ev with
 	     | Some body -> whrec (body, stack)
 	     | None -> s)
       | Const const when red_delta flags ->
@@ -355,7 +357,7 @@ let rec whd_state_gen flags env sigma =
 	    (mkCase (ci, p, app_stack (c,cargs), lf), stack)
             
       | Fix fix when red_iota flags ->
-	  (match reduce_fix whrec fix stack with
+	  (match reduce_fix (fun _ -> whrec) sigma fix stack with
              | Reduced s' -> whrec s'
 	     | NotReducible -> s)
 
@@ -363,7 +365,7 @@ let rec whd_state_gen flags env sigma =
   in 
   whrec
 
-let local_whd_state_gen flags = 
+let local_whd_state_gen flags sigma = 
   let rec whrec (x, stack as s) =
     match kind_of_term x with
       | LetIn (_,b,_,c) when red_zeta flags -> stacklam whrec [b] c stack
@@ -398,105 +400,91 @@ let local_whd_state_gen flags =
 	    (mkCase (ci, p, app_stack (c,cargs), lf), stack)
             
       | Fix fix when red_iota flags ->
-	  (match reduce_fix whrec fix stack with
+	  (match reduce_fix (fun _ ->whrec) sigma fix stack with
              | Reduced s' -> whrec s'
 	     | NotReducible -> s)
 
+      | Evar ev ->
+          (match safe_evar_value sigma ev with
+              Some c -> whrec (c,stack)
+            | None -> s)
+
       | x -> s
   in 
   whrec
 
 
+let stack_red_of_state_red f sigma x =
+  appterm_of_stack (f sigma (x, empty_stack))
+
+let red_of_state_red f sigma x =
+  app_stack (f sigma (x,empty_stack))
+
 (* 1. Beta Reduction Functions *)
 
 let whd_beta_state = local_whd_state_gen beta
-let whd_beta_stack x = appterm_of_stack (whd_beta_state (x, empty_stack))
-let whd_beta x = app_stack (whd_beta_state (x,empty_stack))
+let whd_beta_stack = stack_red_of_state_red whd_beta_state
+let whd_beta = red_of_state_red whd_beta_state
 
 (* Nouveau ! *)
 let whd_betaetalet_state = local_whd_state_gen betaetalet
-let whd_betaetalet_stack x =
-  appterm_of_stack (whd_betaetalet_state (x, empty_stack))
-let whd_betaetalet x = app_stack (whd_betaetalet_state (x,empty_stack))
+let whd_betaetalet_stack = stack_red_of_state_red whd_betaetalet_state
+let whd_betaetalet = red_of_state_red whd_betaetalet_state
 
 let whd_betalet_state = local_whd_state_gen betalet
-let whd_betalet_stack x = appterm_of_stack (whd_betalet_state (x, empty_stack))
-let whd_betalet x = app_stack (whd_betalet_state (x,empty_stack))
+let whd_betalet_stack = stack_red_of_state_red whd_betalet_state
+let whd_betalet = red_of_state_red whd_betalet_state
 
 (* 2. Delta Reduction Functions *)
 
 let whd_delta_state e = whd_state_gen delta e
-let whd_delta_stack env sigma x =
-  appterm_of_stack (whd_delta_state env sigma (x, empty_stack))
-let whd_delta env sigma c =
-  app_stack (whd_delta_state env sigma (c, empty_stack))
+let whd_delta_stack env = stack_red_of_state_red (whd_delta_state env)
+let whd_delta env = red_of_state_red  (whd_delta_state env)
 
 let whd_betadelta_state e = whd_state_gen betadelta e
-let whd_betadelta_stack env sigma x =
-  appterm_of_stack (whd_betadelta_state env sigma (x, empty_stack))
-let whd_betadelta env sigma c =
-  app_stack (whd_betadelta_state env sigma (c, empty_stack))
-
-let whd_betaevar_state e = whd_state_gen betaevar e
-let whd_betaevar_stack env sigma c =
-  appterm_of_stack (whd_betaevar_state env sigma (c, empty_stack))
-let whd_betaevar env sigma c =
-  app_stack (whd_betaevar_state env sigma (c, empty_stack))
+let whd_betadelta_stack env =
+  stack_red_of_state_red (whd_betadelta_state env)
+let whd_betadelta env =
+  red_of_state_red (whd_betadelta_state env)
 
 
 let whd_betadeltaeta_state e = whd_state_gen betadeltaeta e
-let whd_betadeltaeta_stack env sigma x =
-  appterm_of_stack (whd_betadeltaeta_state env sigma (x, empty_stack))
-let whd_betadeltaeta env sigma x = 
-  app_stack (whd_betadeltaeta_state env sigma (x, empty_stack))
+let whd_betadeltaeta_stack env =
+  stack_red_of_state_red (whd_betadeltaeta_state env)
+let whd_betadeltaeta env = 
+  red_of_state_red (whd_betadeltaeta_state env)
 
 (* 3. Iota reduction Functions *)
 
 let whd_betaiota_state = local_whd_state_gen betaiota
-let whd_betaiota_stack x =
-  appterm_of_stack (whd_betaiota_state (x, empty_stack))
-let whd_betaiota x =
-  app_stack (whd_betaiota_state (x, empty_stack))
+let whd_betaiota_stack = stack_red_of_state_red whd_betaiota_state
+let whd_betaiota = red_of_state_red whd_betaiota_state
 
 let whd_betaiotazeta_state = local_whd_state_gen betaiotazeta
-let whd_betaiotazeta_stack x =
-  appterm_of_stack (whd_betaiotazeta_state (x, empty_stack))
-let whd_betaiotazeta x =
-  app_stack (whd_betaiotazeta_state (x, empty_stack))
-
-let whd_betaiotazetaevar_state = whd_state_gen betaiotazetaevar
-let whd_betaiotazetaevar_stack env sigma x =
-  appterm_of_stack (whd_betaiotazetaevar_state env sigma (x, empty_stack))
-let whd_betaiotazetaevar env sigma x =
-  app_stack (whd_betaiotazetaevar_state env sigma (x, empty_stack))
-
-let whd_betaiotaevar_state e = whd_state_gen betaiotaevar e
-let whd_betaiotaevar_stack env sigma x =
-  appterm_of_stack (whd_betaiotaevar_state env sigma (x, empty_stack))
-let whd_betaiotaevar env sigma x = 
-  app_stack (whd_betaiotaevar_state env sigma (x, empty_stack))
+let whd_betaiotazeta_stack = stack_red_of_state_red whd_betaiotazeta_state
+let whd_betaiotazeta = red_of_state_red whd_betaiotazeta_state
 
 let whd_betadeltaiota_state e = whd_state_gen betadeltaiota e
-let whd_betadeltaiota_stack env sigma x =
-  appterm_of_stack (whd_betadeltaiota_state env sigma (x, empty_stack))
-let whd_betadeltaiota env sigma x = 
-  app_stack (whd_betadeltaiota_state env sigma (x, empty_stack))
+let whd_betadeltaiota_stack env =
+  stack_red_of_state_red (whd_betadeltaiota_state env)
+let whd_betadeltaiota env = 
+  red_of_state_red (whd_betadeltaiota_state env)
 
 let whd_betadeltaiotaeta_state e = whd_state_gen betadeltaiotaeta e
-let whd_betadeltaiotaeta_stack env sigma x =
-  appterm_of_stack (whd_betadeltaiotaeta_state env sigma (x, empty_stack))
-let whd_betadeltaiotaeta env sigma x = 
-  app_stack (whd_betadeltaiotaeta_state env sigma (x, empty_stack))
+let whd_betadeltaiotaeta_stack env =
+  stack_red_of_state_red (whd_betadeltaiotaeta_state env)
+let whd_betadeltaiotaeta env = 
+  red_of_state_red (whd_betadeltaiotaeta_state env)
 
 let whd_betadeltaiota_nolet_state e = whd_state_gen betadeltaiota_nolet e
-let whd_betadeltaiota_nolet_stack env sigma x =
-  appterm_of_stack (whd_betadeltaiota_nolet_state env sigma (x, empty_stack))
-let whd_betadeltaiota_nolet env sigma x = 
-  app_stack (whd_betadeltaiota_nolet_state env sigma (x, empty_stack))
+let whd_betadeltaiota_nolet_stack env =
+  stack_red_of_state_red (whd_betadeltaiota_nolet_state env)
+let whd_betadeltaiota_nolet env = 
+  red_of_state_red (whd_betadeltaiota_nolet_state env)
 
 (* 3. Eta reduction Functions *)
 
-let whd_eta c = app_stack (local_whd_state_gen eta (c,empty_stack))
+let whd_eta c = app_stack (local_whd_state_gen eta Evd.empty (c,empty_stack))
 
 (****************************************************************************)
 (*                   Reduction Functions                                    *)
@@ -506,24 +494,25 @@ let whd_eta c = app_stack (local_whd_state_gen eta (c,empty_stack))
 let rec whd_evar sigma c =
   match kind_of_term c with
     | Evar ev ->
-	let d = 
-	  try Some (Evd.existential_value sigma ev)
-	  with NotInstantiatedEvar | Not_found -> None in
-	(match d with Some c -> whd_evar sigma c | None -> c)
+        (match safe_evar_value sigma ev with
+            Some c -> whd_evar sigma c
+          | None -> c)
     | Sort s when is_sort_variable sigma s -> whd_sort_variable sigma c
     | _ -> c
 
-let nf_evar sigma =
-  local_strong (whd_evar sigma)
+let nf_evar =
+  local_strong whd_evar
 
 (* lazy reduction functions. The infos must be created for each term *)
 (* Note by HH [oct 08] : why would it be the job of clos_norm_flags to add
    a [nf_evar] here *)
 let clos_norm_flags flgs env sigma t =
-  norm_val (create_clos_infos flgs env) (inject (nf_evar sigma t))
+  norm_val
+    (create_clos_infos ~evars:(safe_evar_value sigma) flgs env)
+    (inject t)
 
-let nf_beta = clos_norm_flags Closure.beta empty_env Evd.empty
-let nf_betaiota = clos_norm_flags Closure.betaiota empty_env Evd.empty
+let nf_beta = clos_norm_flags Closure.beta empty_env
+let nf_betaiota = clos_norm_flags Closure.betaiota empty_env
 let nf_betadeltaiota env sigma =
   clos_norm_flags Closure.betadeltaiota env sigma
 
@@ -533,7 +522,7 @@ let nf_betadeltaiota env sigma =
    du type checking :
      (fun x => x + x) M
 *)
-let rec whd_betaiotaevar_preserving_vm_cast env sigma t = 	 
+let rec whd_betaiota_preserving_vm_cast env sigma t = 	 
    let rec stacklam_var subst t stack = 	 
      match (decomp_stack stack,kind_of_term t) with 	 
      | Some (h,stacktl), Lambda (_,_,c) -> 	 
@@ -548,7 +537,7 @@ let rec whd_betaiotaevar_preserving_vm_cast env sigma t =
    and whrec (x, stack as s) = 	 
      match kind_of_term x with 	 
        | Evar ev -> 	 
-           (match existential_opt_value sigma ev with 	 
+           (match safe_evar_value sigma ev with 	 
               | Some body -> whrec (body, stack) 	 
               | None -> s) 	 
        | Cast (c,VMcast,t) -> 	 
@@ -574,12 +563,14 @@ let rec whd_betaiotaevar_preserving_vm_cast env sigma t =
    in 	 
    app_stack (whrec (t,empty_stack))
 
-let nf_betaiotaevar_preserving_vm_cast = 
-  strong whd_betaiotaevar_preserving_vm_cast
+let nf_betaiota_preserving_vm_cast = 
+  strong whd_betaiota_preserving_vm_cast
 
 (* lazy weak head reduction functions *)
 let whd_flags flgs env sigma t =
-  whd_val (create_clos_infos flgs env) (inject (nf_evar sigma t))
+  whd_val
+    (create_clos_infos ~evars:(safe_evar_value sigma) flgs env)
+    (inject t)
 
 (********************************************************************)
 (*                         Conversion                               *)
@@ -621,9 +612,9 @@ let nf_red_env sigma env =
     (fun d env -> push_rel (nf_decl d) env) ~init:env ctxt
 
 
-let test_conversion f env sigma x y =
+let test_conversion (f:?evars:'a->'b) env sigma x y =
   try let _ =
-    f (nf_red_env sigma env) (nf_evar sigma x) (nf_evar sigma y) in true
+    f ~evars:(safe_evar_value sigma) env x y in true
   with NotConvertible -> false
 
 let is_conv env sigma = test_conversion Reduction.conv env sigma
@@ -709,7 +700,8 @@ let plain_instance s c =
  *)
 
 let instance s c =
-  (* if s = [] then c else *) local_strong whd_betaiota (plain_instance s c)
+  (* if s = [] then c else *)
+  local_strong whd_betaiota Evd.empty (plain_instance s c)
 
 (* pseudo-reduction rule:
  * [hnf_prod_app env s (Prod(_,B)) N --> B[N]
@@ -820,7 +812,7 @@ let is_sort env sigma arity =
 
 let whd_betaiota_deltazeta_for_iota_state env sigma s =
   let rec whrec s = 
-    let (t, stack as s) = whd_betaiota_state s in
+    let (t, stack as s) = whd_betaiota_state sigma s in
     match kind_of_term t with
     | Case (ci,p,d,lf) ->
         let (cr,crargs) = whd_betadeltaiota_stack env sigma d in
@@ -830,7 +822,7 @@ let whd_betaiota_deltazeta_for_iota_state env sigma s =
         else 
 	  s
     | Fix fix ->
-	  (match reduce_fix (whd_betadeltaiota_state env sigma) fix stack with
+	  (match reduce_fix (whd_betadeltaiota_state env) sigma fix stack with
              | Reduced s -> whrec s
 	     | NotReducible -> s)
     | _ -> s
@@ -872,7 +864,7 @@ let whd_programs_stack env sigma =
 	    else
 	      (mkCase (ci, p, app_stack(c,cargs), lf), stack)
       | Fix fix ->
-	  (match reduce_fix whrec fix stack with
+	  (match reduce_fix (fun _ ->whrec) sigma  fix stack with
              | Reduced s' -> whrec s'
 	     | NotReducible -> s)
       | _ -> s
@@ -942,7 +934,7 @@ let meta_reducible_instance evd b =
     | Some (g,(_,s)) -> (mv,(g.rebus,s))::l 
     | None -> l) [] fm in
   let rec irec u =
-    let u = whd_betaiota u in
+    let u = whd_betaiota Evd.empty u in
     match kind_of_term u with
     | Case (ci,p,c,bl) when isMeta c or isCast c & isMeta (pi1 (destCast c)) ->
 	let m = try destMeta c with _ -> destMeta (pi1 (destCast c)) in
diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli
index 171967583e..535101d743 100644
--- a/pretyping/reductionops.mli
+++ b/pretyping/reductionops.mli
@@ -54,17 +54,18 @@ type state = constr * constr stack
 
 type contextual_reduction_function = env -> evar_map -> constr -> constr
 type reduction_function = contextual_reduction_function
-type local_reduction_function = constr -> constr
+type local_reduction_function = evar_map -> constr -> constr
 
 type contextual_stack_reduction_function = 
     env -> evar_map -> constr -> constr * constr list
 type stack_reduction_function = contextual_stack_reduction_function
-type local_stack_reduction_function = constr -> constr * constr list
+type local_stack_reduction_function =
+    evar_map -> constr -> constr * constr list
 
 type contextual_state_reduction_function = 
     env -> evar_map -> state -> state
 type state_reduction_function = contextual_state_reduction_function
-type local_state_reduction_function = state -> state
+type local_state_reduction_function = evar_map -> state -> state
 
 (* Removes cast and put into applicative form *)
 val whd_stack : local_stack_reduction_function
@@ -92,13 +93,12 @@ val nf_betaiota : local_reduction_function
 val nf_betadeltaiota : reduction_function
 val nf_evar : evar_map -> constr -> constr
 
-val nf_betaiotaevar_preserving_vm_cast : reduction_function
+val nf_betaiota_preserving_vm_cast : reduction_function
 (* Lazy strategy, weak head reduction *)
 val whd_evar :  evar_map -> constr -> constr
 val whd_beta : local_reduction_function
 val whd_betaiota : local_reduction_function
 val whd_betaiotazeta : local_reduction_function
-val whd_betaiotazetaevar : contextual_reduction_function
 val whd_betadeltaiota :  contextual_reduction_function
 val whd_betadeltaiota_nolet :  contextual_reduction_function
 val whd_betaetalet : local_reduction_function
@@ -106,7 +106,7 @@ val whd_betalet : local_reduction_function
 
 val whd_beta_stack : local_stack_reduction_function
 val whd_betaiota_stack : local_stack_reduction_function
-val whd_betaiotazetaevar_stack : contextual_stack_reduction_function
+val whd_betaiotazeta_stack : local_stack_reduction_function
 val whd_betadeltaiota_stack : contextual_stack_reduction_function
 val whd_betadeltaiota_nolet_stack : contextual_stack_reduction_function
 val whd_betaetalet_stack : local_stack_reduction_function
@@ -114,7 +114,7 @@ val whd_betalet_stack : local_stack_reduction_function
 
 val whd_beta_state : local_state_reduction_function
 val whd_betaiota_state : local_state_reduction_function
-val whd_betaiotazetaevar_state : contextual_state_reduction_function
+val whd_betaiotazeta_state : local_state_reduction_function
 val whd_betadeltaiota_state : contextual_state_reduction_function
 val whd_betadeltaiota_nolet_state : contextual_state_reduction_function
 val whd_betaetalet_state : local_state_reduction_function
@@ -128,12 +128,6 @@ val whd_delta :  reduction_function
 val whd_betadelta_stack :  stack_reduction_function
 val whd_betadelta_state :  state_reduction_function
 val whd_betadelta :  reduction_function
-val whd_betaevar_stack :  stack_reduction_function
-val whd_betaevar_state :  state_reduction_function
-val whd_betaevar :  reduction_function
-val whd_betaiotaevar_stack :  stack_reduction_function
-val whd_betaiotaevar_state :  state_reduction_function
-val whd_betaiotaevar :  reduction_function
 val whd_betadeltaeta_stack :  stack_reduction_function
 val whd_betadeltaeta_state :  state_reduction_function
 val whd_betadeltaeta :  reduction_function
@@ -143,8 +137,9 @@ val whd_betadeltaiotaeta :  reduction_function
 
 val whd_eta : constr -> constr
 
+(* Various reduction functions *)
 
-
+val safe_evar_value : evar_map -> existential -> constr option
 
 val beta_applist : constr * constr list -> constr
 
@@ -187,7 +182,7 @@ val whd_programs :  reduction_function
 type fix_reduction_result = NotReducible | Reduced of state
 
 val fix_recarg : fixpoint -> constr stack -> (int * constr) option
-val reduce_fix : local_state_reduction_function -> fixpoint
+val reduce_fix : local_state_reduction_function -> evar_map -> fixpoint
    -> constr stack -> fix_reduction_result
 
 (*s Querying the kernel conversion oracle: opaque/transparent constants *)
diff --git a/pretyping/retyping.ml b/pretyping/retyping.ml
index 2460c7642a..3323c75b48 100644
--- a/pretyping/retyping.ml
+++ b/pretyping/retyping.ml
@@ -62,9 +62,9 @@ let retype sigma metamap =
         let Inductiveops.IndType(_,realargs) =
           try Inductiveops.find_rectype env sigma (type_of env c)
           with Not_found -> anomaly "type_of: Bad recursive type" in
-        let t = whd_beta (applist (p, realargs)) in
+        let t = whd_beta sigma (applist (p, realargs)) in
         (match kind_of_term (whd_betadeltaiota env sigma (type_of env t)) with
-          | Prod _ -> whd_beta (applist (t, [c]))
+          | Prod _ -> whd_beta sigma (applist (t, [c]))
           | _ -> t)
     | Lambda (name,c1,c2) ->
           mkProd (name, c1, type_of (push_rel (name,None,c1) env) c2)
diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml
index 2c2bddb459..cca6b18558 100644
--- a/pretyping/tacred.ml
+++ b/pretyping/tacred.ml
@@ -204,7 +204,7 @@ let invert_name labs l na0 env sigma ref = function
 		| None -> None
 		| Some c -> 
 		    let labs',ccl = decompose_lam c in
-		    let _, l' = whd_betalet_stack ccl in
+		    let _, l' = whd_betalet_stack sigma ccl in
 		    let labs' = List.map snd labs' in
 		    if labs' = labs & l = l' then Some (minfxargs,ref)
                     else None
@@ -234,7 +234,7 @@ let compute_consteval_direct sigma env ref =
 
 let compute_consteval_mutual_fix sigma env ref =
   let rec srec env minarg labs ref c =
-    let c',l = whd_betalet_stack c in
+    let c',l = whd_betalet_stack sigma c in
     let nargs = List.length l in
     match kind_of_term c' with
       | Lambda (na,t,g) when l=[] ->
@@ -378,7 +378,7 @@ let solve_arity_problem env sigma fxminargs c =
   let evm = ref sigma in
   let set_fix i = evm := Evd.define !evm i (mkVar vfx) in
   let rec check strict c =
-    let c' = whd_betaiotazeta c in
+    let c' = whd_betaiotazeta sigma c in
     let (h,rcargs) = decompose_app c' in
     match kind_of_term h with
         Evar(i,_) when Intmap.mem i fxminargs && not (Evd.is_defined !evm i) ->
@@ -418,14 +418,14 @@ let substl_checking_arity env subst c =
 
 
 
-let contract_fix_use_function env f
+let contract_fix_use_function env sigma f
   ((recindices,bodynum),(_names,_types,bodies as typedbodies)) =
   let nbodies = Array.length recindices in
   let make_Fi j = (mkFix((recindices,j),typedbodies), f j) in
   let lbodies = list_tabulate make_Fi nbodies in
-  substl_checking_arity env (List.rev lbodies) (nf_beta bodies.(bodynum))
+  substl_checking_arity env (List.rev lbodies) (nf_beta sigma bodies.(bodynum))
 
-let reduce_fix_use_function env f whfun fix stack =
+let reduce_fix_use_function env sigma f whfun fix stack =
   match fix_recarg fix stack with
     | None -> NotReducible
     | Some (recargnum,recarg) ->
@@ -438,17 +438,18 @@ let reduce_fix_use_function env f whfun fix stack =
         let stack' = stack_assign stack recargnum (app_stack recarg') in
 	(match kind_of_term recarg'hd with
            | Construct _ ->
-	       Reduced (contract_fix_use_function env f fix,stack')
+	       Reduced (contract_fix_use_function env sigma f fix,stack')
 	   | _ -> NotReducible)
 
-let contract_cofix_use_function env f
+let contract_cofix_use_function env sigma f
   (bodynum,(_names,_,bodies as typedbodies)) =
   let nbodies = Array.length bodies in
   let make_Fi j = (mkCoFix(j,typedbodies), f j) in
   let subbodies = list_tabulate make_Fi nbodies in
-  substl_checking_arity env (List.rev subbodies) (nf_beta bodies.(bodynum))
+  substl_checking_arity env (List.rev subbodies)
+    (nf_beta sigma bodies.(bodynum))
 
-let reduce_mind_case_use_function func env mia =
+let reduce_mind_case_use_function func env sigma mia =
   match kind_of_term mia.mconstr with 
     | Construct(ind_sp,i) ->
 	let real_cargs = list_skipn mia.mci.ci_npar mia.mcargs in
@@ -476,11 +477,11 @@ let reduce_mind_case_use_function func env mia =
 	  else
 	    fun _ -> None in
 	let cofix_def =
-          contract_cofix_use_function env build_cofix_name cofix in
+          contract_cofix_use_function env sigma build_cofix_name cofix in
 	mkCase (mia.mci, mia.mP, applist(cofix_def,mia.mcargs), mia.mlf)
     | _ -> assert false
 
-let special_red_case sigma env whfun (ci, p, c, lf)  =
+let special_red_case env sigma whfun (ci, p, c, lf)  =
   let rec redrec s = 
     let (constr, cargs) = whfun s in 
     if isEvalRef env constr then
@@ -489,7 +490,7 @@ let special_red_case sigma env whfun (ci, p, c, lf)  =
         | None -> raise Redelimination
         | Some gvalue ->
 	    if reducible_mind_case gvalue then
-	      reduce_mind_case_use_function constr env
+	      reduce_mind_case_use_function constr env sigma
 	        {mP=p; mconstr=gvalue; mcargs=list_of_stack cargs;
                 mci=ci; mlf=lf}
 	    else
@@ -514,15 +515,15 @@ let rec red_elim_const env sigma ref largs =
 	let c = reference_value sigma env ref in
 	let c', lrest = whd_betadelta_state env sigma (c,largs) in
 	let whfun = whd_simpl_state env sigma in
-        (special_red_case sigma env whfun (destCase c'), lrest)
+        (special_red_case env sigma whfun (destCase c'), lrest)
     | EliminationFix (min,minfxargs,infos) when stack_args_size largs >=min ->
 	let c = reference_value sigma env ref in
 	let d, lrest = whd_betadelta_state env sigma (c,largs) in
 	let f = make_elim_fun ([|Some (minfxargs,ref)|],infos) largs in
 	let whfun = whd_construct_state env sigma in
-	(match reduce_fix_use_function env f whfun (destFix d) lrest with
+	(match reduce_fix_use_function env sigma f whfun (destFix d) lrest with
 	   | NotReducible -> raise Redelimination
-	   | Reduced (c,rest) -> (nf_beta c, rest))
+	   | Reduced (c,rest) -> (nf_beta sigma c, rest))
     | EliminationMutualFix (min,refgoal,refinfos)
 	when stack_args_size largs >= min ->
 	let rec descend ref args =
@@ -530,15 +531,15 @@ let rec red_elim_const env sigma ref largs =
 	  if ref = refgoal then
 	    (c,args)
 	  else
-	    let c', lrest = whd_betalet_state (c,args) in
+	    let c', lrest = whd_betalet_state sigma (c,args) in
 	    descend (destEvalRef c') lrest in
 	let (_, midargs as s) = descend ref largs in
 	let d, lrest = whd_betadelta_state env sigma s in
 	let f = make_elim_fun refinfos midargs in
 	let whfun = whd_construct_state env sigma in
-	(match reduce_fix_use_function env f whfun (destFix d) lrest with
+	(match reduce_fix_use_function env sigma f whfun (destFix d) lrest with
 	   | NotReducible -> raise Redelimination
-	   | Reduced (c,rest) -> (nf_beta c, rest))
+	   | Reduced (c,rest) -> (nf_beta sigma c, rest))
     | _ -> raise Redelimination
 
 (* reduce to whd normal form or to an applied constant that does not hide
@@ -556,11 +557,11 @@ and whd_simpl_state env sigma s =
       | Cast (c,_,_) -> redrec (c, stack)
       | Case (ci,p,c,lf) ->
           (try 
-	    redrec (special_red_case sigma env redrec (ci,p,c,lf), stack)
+	    redrec (special_red_case env sigma redrec (ci,p,c,lf), stack)
 	  with
 	      Redelimination -> s)
       | Fix fix ->
-	  (try match reduce_fix (whd_construct_state env sigma) fix stack with
+	  (try match reduce_fix (whd_construct_state env) sigma fix stack with
             | Reduced s' -> redrec s'
 	    | NotReducible -> s
 	  with Redelimination -> s)
@@ -660,7 +661,7 @@ let whd_simpl_orelse_delta_but_fix_old env sigma c =
       | Cast (c,_,_) -> redrec (c, stack)
       | Case (ci,p,d,lf) ->
           (try
-             redrec (special_red_case sigma env whd_all (ci,p,d,lf), stack)
+             redrec (special_red_case env sigma whd_all (ci,p,d,lf), stack)
            with Redelimination -> 
 	     s)
       | Fix fix ->
@@ -795,7 +796,7 @@ let unfoldoccs env sigma ((nowhere_except_in,locs as plocs),name) c =
       error ((string_of_evaluable_ref env name)^" does not occur.");
     let rest = List.filter (fun o -> o >= nbocc) locs in
     if rest <> [] then error_invalid_occurrence rest;
-    nf_betaiota uc
+    nf_betaiota sigma uc
 
 (* Unfold reduction tactic: *)
 let unfoldn loccname env sigma c = 
@@ -824,10 +825,10 @@ let fold_commands cl env sigma c =
 
 (* call by value reduction functions *)
 let cbv_norm_flags flags env sigma t =
-  cbv_norm (create_cbv_infos flags env) (nf_evar sigma t)
+  cbv_norm (create_cbv_infos flags env sigma) t
 
-let cbv_beta = cbv_norm_flags beta empty_env Evd.empty
-let cbv_betaiota = cbv_norm_flags betaiota empty_env Evd.empty
+let cbv_beta = cbv_norm_flags beta empty_env
+let cbv_betaiota = cbv_norm_flags betaiota empty_env
 let cbv_betadeltaiota env sigma =  cbv_norm_flags betadeltaiota env sigma
 
 let compute = cbv_betadeltaiota
@@ -899,11 +900,11 @@ let one_step_reduce env sigma c =
       | Cast (c,_,_) -> redrec (c,stack)
       | Case (ci,p,c,lf) ->
           (try
-	     (special_red_case sigma env (whd_simpl_state env sigma)
+	     (special_red_case env sigma (whd_simpl_state env sigma)
 	       (ci,p,c,lf), stack)
            with Redelimination -> raise NotStepReducible)
       | Fix fix ->
-	  (match reduce_fix (whd_construct_state env sigma) fix stack with
+	  (match reduce_fix (whd_construct_state env) sigma fix stack with
              | Reduced s' -> s'
 	     | NotReducible -> raise NotStepReducible)
       | _ when isEvalRef env x ->
@@ -932,7 +933,7 @@ let reduce_to_ref_gen allow_product env sigma ref t =
   else
   (* lazily reduces to match the head of [t] with the expected [ref] *)
   let rec elimrec env t l = 
-    let c, _ = Reductionops.whd_stack t in
+    let c, _ = Reductionops.whd_stack sigma t in
     match kind_of_term c with
       | Prod (n,ty,t') ->
 	  if allow_product then
@@ -948,7 +949,7 @@ let reduce_to_ref_gen allow_product env sigma ref t =
 	    else raise Not_found
 	  with Not_found ->
           try 
-	    let t' = nf_betaiota (one_step_reduce env sigma t) in 
+	    let t' = nf_betaiota sigma (one_step_reduce env sigma t) in 
 	    elimrec env t' l
           with NotStepReducible ->
 	    errorlabstrm ""
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index 102d918fb7..54421f96f8 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -268,21 +268,25 @@ let unify_0_with_initial_metas subst conv_at_top env sigma cv_pb flags m n =
 	| Some true -> 
 	    (match expand_key curenv cf1 with
 	    | Some c ->
-		unirec_rec curenvnb pb b substn (whd_betaiotazeta (mkApp(c,l1))) cN
+		unirec_rec curenvnb pb b substn
+                  (whd_betaiotazeta sigma (mkApp(c,l1))) cN
 	    | None ->
 		(match expand_key curenv cf2 with
 		| Some c ->
-		    unirec_rec curenvnb pb b substn cM (whd_betaiotazeta (mkApp(c,l2)))
+		    unirec_rec curenvnb pb b substn cM
+                      (whd_betaiotazeta sigma (mkApp(c,l2)))
 		| None ->
 		    error_cannot_unify curenv sigma (cM,cN)))
 	| Some false ->
 	    (match expand_key curenv cf2 with
 	    | Some c ->
-		unirec_rec curenvnb pb b substn cM (whd_betaiotazeta (mkApp(c,l2)))
+		unirec_rec curenvnb pb b substn cM
+                  (whd_betaiotazeta sigma (mkApp(c,l2)))
 	    | None ->
 		(match expand_key curenv cf1 with
 		| Some c ->
-		    unirec_rec curenvnb pb b substn (whd_betaiotazeta (mkApp(c,l1))) cN
+		    unirec_rec curenvnb pb b substn
+                      (whd_betaiotazeta sigma (mkApp(c,l1))) cN
 		| None ->
 		    error_cannot_unify curenv sigma (cM,cN)))
     else
@@ -489,7 +493,7 @@ let unify_to_type env evd flags c u =
   let sigma = evars_of evd in
   let c = refresh_universes c in
   let t = get_type_of_with_meta env sigma (metas_of evd) c in
-  let t = Tacred.hnf_constr env sigma (nf_betaiota (nf_meta evd t)) in
+  let t = Tacred.hnf_constr env sigma (nf_betaiota sigma (nf_meta evd t)) in
   let u = Tacred.hnf_constr env sigma u in
   try unify_0 env sigma Cumul flags t u
   with e when precatchable_exception e -> ([],[])
@@ -613,11 +617,12 @@ let w_unify_meta_types env ?(flags=default_unify_flags) evd =
    types of metavars are unifiable with the types of their instances    *)
 
 let check_types env evd flags subst m n =
-  if isEvar (fst (whd_stack m)) or isEvar (fst (whd_stack n)) then
+  let sigma = evars_of evd in
+  if isEvar (fst (whd_stack sigma m)) or isEvar (fst (whd_stack sigma n)) then
     unify_0_with_initial_metas subst true env (evars_of evd) topconv 
       flags
-      (Retyping.get_type_of_with_meta env (evars_of evd) (metas_of evd) m)
-      (Retyping.get_type_of_with_meta env (evars_of evd) (metas_of evd) n)
+      (Retyping.get_type_of_with_meta env sigma (metas_of evd) m)
+      (Retyping.get_type_of_with_meta env sigma (metas_of evd) n)
   else
     subst
 
@@ -738,8 +743,8 @@ let secondOrderAbstraction env flags allow_K typ (p, oplist) evd =
   w_merge env false flags ([p,pred,(ConvUpToEta 0,TypeProcessed)],[]) evd'
 
 let w_unify2 env flags allow_K cv_pb ty1 ty2 evd =
-  let c1, oplist1 = whd_stack ty1 in
-  let c2, oplist2 = whd_stack ty2 in
+  let c1, oplist1 = whd_stack (evars_of evd) ty1 in
+  let c2, oplist2 = whd_stack (evars_of evd) ty2 in
   match kind_of_term c1, kind_of_term c2 with
     | Meta p1, _ ->
         (* Find the predicate *)
@@ -777,8 +782,8 @@ let w_unify2 env flags allow_K cv_pb ty1 ty2 evd =
    Meta(1) had meta-variables in it. *)
 let w_unify allow_K env cv_pb ?(flags=default_unify_flags) ty1 ty2 evd =
   let cv_pb = of_conv_pb cv_pb in
-  let hd1,l1 = whd_stack ty1 in
-  let hd2,l2 = whd_stack ty2 in
+  let hd1,l1 = whd_stack (evars_of evd) ty1 in
+  let hd2,l2 = whd_stack (evars_of evd) ty2 in
     match kind_of_term hd1, l1<>[], kind_of_term hd2, l2<>[] with
       (* Pattern case *)
       | (Meta _, true, Lambda _, _ | Lambda _, _, Meta _, true)