- when List.length args > recno -> could_reduce (List.nth args recno)
- | C.Match (_,_,arg,_) -> could_reduce arg
- | C.Appl (he::_) -> could_reduce he
+ when List.length args > recno ->
+ let t = NCicReduction.whd status ~subst context (List.nth args recno) in
+ could_reduce status subst context t
+ | C.Match (_,_,arg,_) -> could_reduce status ~subst context arg
+ | C.Appl (he::_) -> could_reduce status ~subst context he