exception Subst_not_found of int
exception Meta_not_found of int
-let head_beta_reduce = ref (fun _ ~upto:_ _ -> assert false);;
+let head_beta_reduce = ref (fun (_:NCicEnvironment.status) ~upto:_ _ -> assert false);;
let set_head_beta_reduce = (:=) head_beta_reduce;;
let expand_local_context = 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 _
| C.Appl l :: tl -> C.Appl (l@tl)
| l1 -> C.Appl l1
in
- if fire_beta then !head_beta_reduce (status :> NCic.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