Defs in context may now have an optional type (when unknown).

[helm.git] / helm / ocaml / cic_omdoc / eta_fixing.ml

diff --git a/helm/ocaml/cic_omdoc/eta_fixing.ml b/helm/ocaml/cic_omdoc/eta_fixing.ml
index 81668203dab55673c8fb2ab74c2ebbcac9a0753f..d6293d2434ad61af36b7c94203a0cf7b6c8641c7 100644 (file)
--- 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 in
+              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