;;
let apply_subst =
-(* CSC: old code that never performs beta reduction
- let appl_fun um_aux he tl =
- let tl' = List.map um_aux tl in
- begin
- match um_aux he with
- Cic.Appl l -> Cic.Appl (l@tl')
- | he' -> Cic.Appl (he'::tl')
- end
- in
- apply_subst_gen ~appl_fun
-*)
let appl_fun um_aux he tl =
let tl' = List.map um_aux tl in
let t' =
in
begin
match he with
- Cic.Meta (m,_) ->
- let rec beta_reduce =
- function
- (Cic.Appl (Cic.Lambda (_,_,t)::he'::tl')) ->
- let he'' = CicSubstitution.subst he' t in
- if tl' = [] then
- he''
- else
- beta_reduce (Cic.Appl(he''::tl'))
- | t -> t
- in
- beta_reduce t'
+ Cic.Meta (m,_) -> CicReduction.head_beta_reduce t'
| _ -> t'
end
in