pushed evar reduction in kernel

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

5 files changed, 13 insertions, 11 deletions

diff --git a/tactics/class_tactics.ml4 b/tactics/class_tactics.ml4
index 4eb20cb53e..9d8b6c3b57 100644
--- a/tactics/class_tactics.ml4
+++ b/tactics/class_tactics.ml4
@@ -650,14 +650,14 @@ let build_signature isevars env m (cstrs : 'a option list) (finalcstr : 'a Lazy.
       | Prod (na, ty, b), obj :: cstrs -> 
 	  if dependent (mkRel 1) b then
 	    let (b, arg, evars) = aux (Environ.push_rel (na, None, ty) env) b cstrs in
-	    let ty = Reductionops.nf_betaiota ty in
+	    let ty = Reductionops.nf_betaiota (Evd.evars_of !isevars) ty in
 	    let pred = mkLambda (na, ty, b) in
 	    let liftarg = mkLambda (na, ty, arg) in
 	    let arg' = mkApp (Lazy.force forall_relation, [| ty ; pred ; liftarg |]) in
 	      mkProd(na, ty, b), arg', (ty, None) :: evars
 	  else
 	    let (b', arg, evars) = aux env (subst1 mkProp b) cstrs in
-	    let ty = Reductionops.nf_betaiota ty in
+	    let ty = Reductionops.nf_betaiota(Evd.evars_of !isevars) ty in
 	    let relty = mk_relty ty obj in
 	    let newarg = mkApp (Lazy.force respectful, [| ty ; b' ; relty ; arg |]) in
 	      mkProd(na, ty, b), newarg, (ty, Some relty) :: evars
@@ -665,7 +665,7 @@ let build_signature isevars env m (cstrs : 'a option list) (finalcstr : 'a Lazy.
       | _, [] -> 
 	  (match finalcstr with
 	      None -> 
-		let t = Reductionops.nf_betaiota ty in
+		let t = Reductionops.nf_betaiota(Evd.evars_of !isevars) ty in
 		let rel = mk_relty t None in 
 		  t, rel, [t, Some rel]
 	    | Some codom -> let (t, rel) = Lazy.force codom in
diff --git a/tactics/decl_proof_instr.ml b/tactics/decl_proof_instr.ml
index 7e25b072ea..967bc88e8c 100644
--- a/tactics/decl_proof_instr.ml
+++ b/tactics/decl_proof_instr.ml
@@ -1093,7 +1093,7 @@ let thesis_for obj typ per_info env=
       ((Printer.pr_constr_env env obj) ++ spc () ++ 
 	 str "cannot give an induction hypothesis (wrong parameters).") in
   let hd2 = (applist ((lift (List.length rc) per_info.per_pred),args@[obj])) in
-    compose_prod rc (whd_beta hd2)
+    compose_prod rc (whd_beta Evd.empty hd2)
 
 let rec build_product_dep pat_info per_info args body gls =
   match args with 
@@ -1225,7 +1225,7 @@ let hrec_for fix_id per_info gls obj_id =
     try List.for_all2 eq_constr params per_info.per_params with 
         Invalid_argument _ -> false end;
   let hd2 = applist (mkVar fix_id,args@[obj]) in 
-    compose_lam rc (whd_beta hd2)
+    compose_lam rc (whd_beta gls.sigma hd2)
 
 let rec execute_cases fix_name per_info tacnext args objs nhrec tree gls =
   match tree, objs  with
diff --git a/tactics/equality.ml b/tactics/equality.ml
index 721623c912..dd9f648caa 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -120,7 +120,7 @@ let general_rewrite_ebindings_clause cls lft2rgt occs ((c,l) : open_constr with_
     let sigma, c' = c in
     let sigma = Evd.merge sigma (project gl) in
     let ctype = get_type_of env sigma c' in 
-    let rels, t = decompose_prod (whd_betaiotazeta ctype) in
+    let rels, t = decompose_prod (whd_betaiotazeta sigma ctype) in
       match match_with_equality_type t with
       | Some (hdcncl,args) -> (* Fast path: direct leibniz rewrite *)
 	  let lft2rgt = adjust_rewriting_direction args lft2rgt in
@@ -739,7 +739,7 @@ let sig_clausal_form env sigma sort_of_ty siglen ty dflt =
       else
 	error "Cannot solve an unification problem."
     else
-      let (a,p_i_minus_1) = match whd_beta_stack p_i with
+      let (a,p_i_minus_1) = match whd_beta_stack (evars_of !evdref) p_i with
 	| (_sigS,[a;p]) -> (a,p)
  	| _ -> anomaly "sig_clausal_form: should be a sigma type" in
       let ev = Evarutil.e_new_evar evdref env a in
diff --git a/tactics/leminv.ml b/tactics/leminv.ml
index c1f20e8c35..1046ecbf0e 100644
--- a/tactics/leminv.ml
+++ b/tactics/leminv.ml
@@ -237,7 +237,8 @@ let inversion_scheme env sigma t sort dep_option inv_op =
       meta_types 
   in
   let invProof = 
-    it_mkNamedLambda_or_LetIn (local_strong (whd_meta mvb) pfterm) ownSign 
+    it_mkNamedLambda_or_LetIn
+      (local_strong (fun _ -> whd_meta mvb) Evd.empty pfterm) ownSign 
   in
   invProof
 
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index caef1c94a6..527b66c9e1 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -753,7 +753,7 @@ let general_apply with_delta with_destruct with_evars (c,lbind) gl0 =
   let concl_nprod = nb_prod (pf_concl gl0) in
   let evm, c = c in
   let rec try_main_apply c gl =
-    let thm_ty0 = nf_betaiota (pf_type_of gl c) in
+    let thm_ty0 = nf_betaiota (project gl) (pf_type_of gl c) in
     let try_apply thm_ty nprod =
       let n = nb_prod thm_ty - nprod in
 	if n<0 then error "Applied theorem has not enough premisses.";
@@ -844,7 +844,7 @@ let progress_with_clause flags innerclause clause =
   with Failure _ -> error "Unable to unify."
 
 let apply_in_once_main flags innerclause (d,lbind) gl =
-  let thm = nf_betaiota (pf_type_of gl d) in
+  let thm = nf_betaiota gl.sigma (pf_type_of gl d) in
   let rec aux clause =
     try progress_with_clause flags innerclause clause
     with err ->
@@ -979,7 +979,8 @@ let specialize mopt (c,lbind) g =
     else 
       let clause = make_clenv_binding g (c,pf_type_of g c) lbind in
       let clause = clenv_unify_meta_types clause in
-      let (thd,tstack) = whd_stack (clenv_value clause) in
+      let (thd,tstack) =
+        whd_stack (evars_of clause.evd) (clenv_value clause) in
       let nargs = List.length tstack in
       let tstack = match mopt with 
 	| Some m ->