| C.Rel _ as t -> a,t
| C.Appl [] | C.Appl [_] -> assert false
| C.Appl l as orig ->
+ let fire_beta, upto =
+ match l with C.Meta _ :: _ -> true, List.length l - 1 | _ -> false, 0
+ in
let a,l1 =
(* sharing fold? *)
List.fold_right
(fun t (a,l) -> let a,t = f k a t in a, t :: l)
l (a,[])
in
- a, if l1 == l then orig else (match l1 with
- | C.Appl l :: tl -> C.Appl (l@tl)
- | _ -> C.Appl l1)
+ a, if l1 == l then orig else
+ let t =
+ match l1 with
+ | C.Appl l :: tl -> C.Appl (l@tl)
+ | _ -> C.Appl l1
+ in
+ if fire_beta then NCicReduction.head_beta_reduce ~upto t
+ else t
| C.Prod (n,s,t) as orig ->
let a,s1 = f k a s in let a,t1 = f (g (n,C.Decl s) k) a t in
a, if t1 == t && s1 == s then orig else C.Prod (n,s1,t1)