(fun (_,t) i -> i && guarded_by_destructors context n nn kl x safes t)
exp_named_subst true
| C.MutCase (uri,i,outtype,term,pl) ->
- (match term with
+ (match CicReduction.whd context term with
C.Rel m when List.mem m safes || m = x ->
let (tys,len,isinductive,paramsno,cl) =
let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in