pushed evar reduction in kernel

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

8 files changed, 27 insertions, 24 deletions

diff --git a/contrib/extraction/extraction.ml b/contrib/extraction/extraction.ml
index f290fea810..ffaefd5e38 100644
--- a/contrib/extraction/extraction.ml
+++ b/contrib/extraction/extraction.ml
@@ -177,7 +177,7 @@ let parse_ind_args si args relmax =
 
 
 let rec extract_type env db j c args =
-  match kind_of_term (whd_betaiotazeta c) with
+  match kind_of_term (whd_betaiotazeta Evd.empty c) with
     | App (d, args') ->
 	(* We just accumulate the arguments. *)
 	extract_type env db j d (Array.to_list args' @ args)
@@ -285,7 +285,7 @@ and extract_type_app env db (r,s) args =
 and extract_type_scheme env db c p =
   if p=0 then extract_type env db 0 c []
   else
-    let c = whd_betaiotazeta c in
+    let c = whd_betaiotazeta Evd.empty c in
     match kind_of_term c with
       | Lambda (n,t,d) ->
           extract_type_scheme (push_rel_assum (n,t) env) db d (p-1)
diff --git a/contrib/firstorder/unify.ml b/contrib/firstorder/unify.ml
index 41a100c2b1..782129e5c9 100644
--- a/contrib/firstorder/unify.ml
+++ b/contrib/firstorder/unify.ml
@@ -42,8 +42,8 @@ let unif t1 t2=
     Queue.add (t1,t2) bige;
     try while true do
       let t1,t2=Queue.take bige in
-      let nt1=head_reduce (whd_betaiotazeta t1) 
-      and nt2=head_reduce (whd_betaiotazeta t2) in
+      let nt1=head_reduce (whd_betaiotazeta Evd.empty t1) 
+      and nt2=head_reduce (whd_betaiotazeta Evd.empty t2) in
 	match (kind_of_term nt1),(kind_of_term nt2) with
 	    Meta i,Meta j-> 
 	      if i<>j then 
diff --git a/contrib/funind/functional_principles_proofs.ml b/contrib/funind/functional_principles_proofs.ml
index b9b47fde11..75b811d518 100644
--- a/contrib/funind/functional_principles_proofs.ml
+++ b/contrib/funind/functional_principles_proofs.ml
@@ -293,7 +293,8 @@ let change_eq env sigma hyp_id (context:rel_context) x t end_of_type  =
 	(new_end_of_type,0,witness_fun)
 	context
     in
-    let new_type_of_hyp = Reductionops.nf_betaiota  new_type_of_hyp in 
+    let new_type_of_hyp =
+      Reductionops.nf_betaiota Evd.empty new_type_of_hyp in 
     let new_ctxt,new_end_of_type = 
       decompose_prod_n_assum ctxt_size new_type_of_hyp 
     in 
@@ -759,7 +760,8 @@ let build_proof
 		  | Const _ ->
 		      do_finalize dyn_infos  g
 		  | Lambda _ -> 
-		      let new_term = Reductionops.nf_beta dyn_infos.info in 
+		      let new_term =
+                        Reductionops.nf_beta Evd.empty dyn_infos.info in 
 		      build_proof do_finalize {dyn_infos with info = new_term} 
 			g
 		  | LetIn _ -> 
@@ -1107,7 +1109,7 @@ let prove_princ_for_struct interactive_proof fun_num fnames all_funs _nparams :
 	    let bodies_with_all_params = 
 	      Array.map 
 		(fun body -> 
-		   Reductionops.nf_betaiota 
+		   Reductionops.nf_betaiota Evd.empty
 		     (applist(substl (List.rev (Array.to_list all_funs_with_full_params)) body,
 			      List.rev_map var_of_decl princ_params))
 		)
@@ -1144,12 +1146,12 @@ let prove_princ_for_struct interactive_proof fun_num fnames all_funs _nparams :
 		   let body_with_param,num = 
 		     let body = get_body fnames.(i) in 
 		     let body_with_full_params = 
-		       Reductionops.nf_betaiota (
+		       Reductionops.nf_betaiota Evd.empty (
 			 applist(body,List.rev_map var_of_decl full_params))
 		     in
 		     match kind_of_term body_with_full_params with 
 		       | Fix((_,num),(_,_,bs)) -> 
-			       Reductionops.nf_betaiota
+			       Reductionops.nf_betaiota Evd.empty
 				 (
 				   (applist
 				      (substl 
@@ -1225,7 +1227,7 @@ let prove_princ_for_struct interactive_proof fun_num fnames all_funs _nparams :
 		     nb_rec_hyps = -100;
 		     rec_hyps = [];
 		     info = 
-		       Reductionops.nf_betaiota 
+		       Reductionops.nf_betaiota Evd.empty
 			 (applist(fix_body,List.rev_map mkVar args_id));
 		     eq_hyps = []
 		   }
@@ -1287,7 +1289,7 @@ let prove_princ_for_struct interactive_proof fun_num fnames all_funs _nparams :
 		     nb_rec_hyps = -100;
 		     rec_hyps = [];
 		     info = 
-		       Reductionops.nf_betaiota 
+		       Reductionops.nf_betaiota Evd.empty 
 			 (applist(fbody_with_full_params,
 				  (List.rev_map var_of_decl princ_params)@
 				    (List.rev_map mkVar args_id)
diff --git a/contrib/interface/showproof.ml b/contrib/interface/showproof.ml
index cf861642db..2ab62763d4 100644
--- a/contrib/interface/showproof.ml
+++ b/contrib/interface/showproof.ml
@@ -1361,7 +1361,7 @@ and natural_cutintro ig lh g gs arg ltree =
                        {ihsg=No_subgoals_hyp;isgintro=""}
                        (List.nth ltree 0))]
         ]
-and whd_betadeltaiota x = whd_betaiotaevar (Global.env()) Evd.empty x
+and whd_betadeltaiota x = whd_betaiota Evd.empty x
 and type_of_ast s c = type_of (Global.env()) Evd.empty (constr_of_ast c)
 and prod_head t =
   match (kind_of_term (strip_outer_cast t)) with 
diff --git a/contrib/subtac/subtac_cases.ml b/contrib/subtac/subtac_cases.ml
index 3e80be65ef..09ee456d7c 100644
--- a/contrib/subtac/subtac_cases.ml
+++ b/contrib/subtac/subtac_cases.ml
@@ -822,7 +822,7 @@ let infer_predicate loc env isevars typs cstrs indf =
     (* Empiric normalization: p may depend in a irrelevant way on args of the*)
     (* cstr as in [c:{_:Alpha & Beta}] match c with (existS a b)=>(a,b) end *)
     let typs =
-      Array.map (local_strong (whd_betaevar empty_env (Evd.evars_of !isevars))) typs
+      Array.map (local_strong whd_beta (Evd.evars_of !isevars)) typs
     in
     let eqns = array_map2 prepare_unif_pb typs cstrs in
     (* First strategy: no dependencies at all *)
@@ -1042,9 +1042,10 @@ let find_predicate loc env isevars p typs cstrs current
     match p with
       | Some p -> abstract_predicate env (Evd.evars_of !isevars) indf current tms p
       | None -> infer_predicate loc env isevars typs cstrs indf in
-  let typ = whd_beta (applist (pred, realargs)) in
+  let typ = whd_beta (Evd.evars_of !isevars) (applist (pred, realargs)) in
   if dep then
-    (pred, whd_beta (applist (typ, [current])), new_Type ())
+    (pred, whd_beta (Evd.evars_of !isevars) (applist (typ, [current])),
+     new_Type ())
   else
     (pred, typ, new_Type ())
 
@@ -1246,7 +1247,7 @@ and match_current pb tomatch =
 	    find_predicate pb.caseloc pb.env pb.isevars 
 	      pb.pred brtyps cstrs current indt 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 }
diff --git a/contrib/subtac/subtac_obligations.ml b/contrib/subtac/subtac_obligations.ml
index df700e1b1f..8b8bb9ab47 100644
--- a/contrib/subtac/subtac_obligations.ml
+++ b/contrib/subtac/subtac_obligations.ml
@@ -288,7 +288,7 @@ let declare_obligation obl body =
 	print_message (Subtac_utils.definition_message obl.obl_name);
 	{ obl with obl_body = Some (mkConst constant) }
 	  
-let red = Reductionops.nf_betaiota
+let red = Reductionops.nf_betaiota Evd.empty
 
 let init_prog_info n b t deps fixkind notations obls impls kind hook =
   let obls' = 
diff --git a/contrib/xml/cic2acic.ml b/contrib/xml/cic2acic.ml
index c62db00bb1..13e5e6d5fb 100644
--- a/contrib/xml/cic2acic.ml
+++ b/contrib/xml/cic2acic.ml
@@ -245,9 +245,9 @@ let typeur sigma metamap =
         let Inductiveops.IndType(_,realargs) =
           try Inductiveops.find_rectype env sigma (type_of env c)
           with Not_found -> Util.anomaly "type_of: Bad recursive type" in
-        let t = Reductionops.whd_beta (T.applist (p, realargs)) in
+        let t = Reductionops.whd_beta sigma (T.applist (p, realargs)) in
         (match Term.kind_of_term (DoubleTypeInference.whd_betadeltaiotacprop env sigma (type_of env t)) with
-          | T.Prod _ -> Reductionops.whd_beta (T.applist (t, [c]))
+          | T.Prod _ -> Reductionops.whd_beta sigma (T.applist (t, [c]))
           | _ -> t)
     | T.Lambda (name,c1,c2) ->
           T.mkProd (name, c1, type_of (Environ.push_rel (name,None,c1) env) c2)
@@ -390,7 +390,7 @@ Pp.ppnl (Pp.(++) (Pp.str "BUG: this subterm was not visited during the double-ty
           (* We need to refresh the universes because we are doing *)
           (* type inference on an already inferred type.           *)
           {D.synthesized =
-            Reductionops.nf_beta
+            Reductionops.nf_beta evar_map
              (CPropRetyping.get_type_of env evar_map
               (Termops.refresh_universes tt)) ;
            D.expected = None}
diff --git a/contrib/xml/doubleTypeInference.ml b/contrib/xml/doubleTypeInference.ml
index de8c540caf..17d1d5dab4 100644
--- a/contrib/xml/doubleTypeInference.ml
+++ b/contrib/xml/doubleTypeInference.ml
@@ -163,7 +163,7 @@ let double_type_of env sigma cstr expectedty subterms_to_types =
            | hj::restjl ->
               match T.kind_of_term (Reduction.whd_betadeltaiota env typ) with
                  T.Prod (_,c1,c2) ->
-                  (Some (Reductionops.nf_beta c1)) ::
+                  (Some (Reductionops.nf_beta sigma c1)) ::
                    (aux (T.subst1 hj c2) restjl)
                | _ -> assert false
          in
@@ -183,7 +183,7 @@ let double_type_of env sigma cstr expectedty subterms_to_types =
           | Some ety ->
               match T.kind_of_term (Reduction.whd_betadeltaiota env ety) with
                  T.Prod (_,_,expected_target_type) ->
-                  Some (Reductionops.nf_beta expected_target_type)
+                  Some (Reductionops.nf_beta sigma expected_target_type)
                | _ -> assert false
         in
         let j' = execute env1 sigma c2 expectedc2type in 
@@ -214,14 +214,14 @@ let double_type_of env sigma cstr expectedty subterms_to_types =
           Typeops.judge_of_letin env name j1 j2 j3
   
      | T.Cast (c,k,t) ->
-        let cj = execute env sigma c (Some (Reductionops.nf_beta t)) in
+        let cj = execute env sigma c (Some (Reductionops.nf_beta sigma t)) in
         let tj = execute env sigma t None in
 	let tj = type_judgment env sigma tj in
         let j, _ = Typeops.judge_of_cast env cj k tj in
 	 j
     in
      let synthesized = E.j_type judgement in
-     let synthesized' = Reductionops.nf_beta synthesized in
+     let synthesized' = Reductionops.nf_beta sigma synthesized in
       let types,res =
        match expectedty with
           None ->