pushed evar reduction in kernel

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

2 files changed, 7 insertions, 7 deletions

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 ->