if noparams = 0 then
List.map (fun (_,t) -> t) constructors
else
- let term_type =
- TypeInference.type_of_aux' metasenv context term in
+ let term_type =
+ CicTypeChecker.type_of_aux' metasenv context term
+ in
(match term_type with
C.Appl (hd::params) ->
List.map (fun (_,t) -> clean_up t params) constructors