"unit (* TOO POLYMORPHIC TYPE *)"
else (
let needs_obj_magic =
- match ty with
+ (* BUG HERE: we should consider also the right parameters *)
+ match CicReduction.whd context ty with
Cic.Lambda (_,_,t) -> not (DoubleTypeInference.does_not_occur 1 t)
- | _ -> assert false
+ | _ -> false (* it can be a Rel, e.g. in *_rec *)
in
(match analyze_term context te with
`Type -> assert false