X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matitaB%2Fcomponents%2Fng_kernel%2FnCicUtils.ml;h=13fbb586f2dd044ba55666993b312fd8bb46ff22;hb=c3f800643c30f4202164788deda575a40ff2eb8e;hp=400d693638f880366da93bffe5b187b24eea2933;hpb=4f3b04e9966484011328d5b0eb358da4416e29b0;p=helm.git

diff --git a/matitaB/components/ng_kernel/nCicUtils.ml b/matitaB/components/ng_kernel/nCicUtils.ml
index 400d69363..13fbb586f 100644
--- a/matitaB/components/ng_kernel/nCicUtils.ml
+++ b/matitaB/components/ng_kernel/nCicUtils.ml
@@ -56,7 +56,7 @@ let fold g k f acc = function
  | C.Match (_,oty,t,pl) -> List.fold_left (f k) (f k (f k acc oty) t) pl
 ;;
 
-let map status g k f = function
+let map ?(hbr=true) status g k f = function
  | C.Meta _ -> assert false
  | C.Implicit _
  | C.Sort _
@@ -74,7 +74,7 @@ let map status g k f = function
       | C.Appl l :: tl -> C.Appl (l@tl)
       | l1 -> C.Appl l1
     in
-      if fire_beta then !head_beta_reduce (status :> NCicEnvironment.status) ~upto t
+      if fire_beta & hbr then !head_beta_reduce (status :> NCicEnvironment.status) ~upto t
       else t
  | C.Prod (n,s,t) as orig ->
      let s1 = f k s in let t1 = f (g (n,C.Decl s) k) t in