X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_omdoc%2Feta_fixing.ml;h=c224bcf65ad1fb25b7c36d6739ccd996ff94e644;hb=0de1b960f42ac368414b7405a79e7933445ee8af;hp=d6293d2434ad61af36b7c94203a0cf7b6c8641c7;hpb=c706b1cb2c7cbdd23a3281d35d3f0b10c3a684cf;p=helm.git diff --git a/helm/ocaml/cic_omdoc/eta_fixing.ml b/helm/ocaml/cic_omdoc/eta_fixing.ml index d6293d243..c224bcf65 100644 --- a/helm/ocaml/cic_omdoc/eta_fixing.ml +++ b/helm/ocaml/cic_omdoc/eta_fixing.ml @@ -260,8 +260,9 @@ let eta_fix metasenv t = if noparams = 0 then List.map (fun (_,t) -> t) constructors else - let term_type = - CicTypeChecker.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