(*CSC: type-inference, but the result is very poort. As a very weak *)
(*CSC: patch, I apply whd to the computed type. Full beta *)
(*CSC: reduction would be a much better option. *)
- let innertype = CicReduction.whd (T.type_of_aux' metasenv cicenv tt) in
+ let innertype =
+ CicReduction.whd cicenv (T.type_of_aux' metasenv cicenv tt)
+ in
let innersort = T.type_of_aux' metasenv cicenv innertype in
let ainnertype =
if computeinnertypes then