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