;;
let rec flexible_arg context subst = function
- | NCic.Meta (i,_) | NCic.Appl (NCic.Meta (i,_) :: _)->
+ | NCic.Meta (i,_) ->
(try
let _,_,t,_ = List.assoc i subst in
flexible_arg context subst t
with Not_found -> true)
+ | NCic.Appl (NCic.Meta (i,_) :: args)->
+ (try
+ let _,_,t,_ = List.assoc i subst in
+ flexible_arg context subst
+ (NCicReduction.head_beta_reduce ~delta:max_int
+ (NCic.Appl (t :: args)))
+ with Not_found -> true)
(* this is a cheap whd, it only performs zeta-reduction.
*
* it works when the **omissis** disambiguation algorithm