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=4a529a2bc54c536e873075d0715e209ba082aabc;hpb=7c400087e8397459ebe3b932b4710cffcc07a36e;p=helm.git

diff --git a/helm/ocaml/cic_omdoc/eta_fixing.ml b/helm/ocaml/cic_omdoc/eta_fixing.ml
index 4a529a2bc..c224bcf65 100644
--- a/helm/ocaml/cic_omdoc/eta_fixing.ml
+++ b/helm/ocaml/cic_omdoc/eta_fixing.ml
@@ -261,7 +261,7 @@ let eta_fix metasenv t =
             List.map (fun (_,t) -> t) constructors 
           else 
 	         let term_type = 
-            TypeInference.type_of_aux' metasenv context term
+            CicTypeChecker.type_of_aux' metasenv context term
            in
             (match term_type with
                C.Appl (hd::params) ->