- could_reduce status subst context t
- | C.Match (_,_,arg,_) -> could_reduce status ~subst context arg
+ could_reduce status ~subst context t
+ | C.Match (_,_,he,_) ->
+ let he = NCicReduction.whd status ~subst context he in
+ could_reduce status ~subst context he