]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/ocaml/cic_omdoc/eta_fixing.ml
removed dependency on netclient, use http_client module from ocaml-http
[helm.git] / helm / ocaml / cic_omdoc / eta_fixing.ml
index 81668203dab55673c8fb2ab74c2ebbcac9a0753f..c224bcf65ad1fb25b7c36d6739ccd996ff94e644 100644 (file)
@@ -260,8 +260,9 @@ let eta_fix metasenv t =
           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