From: Ferruccio Guidi Date: Tue, 23 Sep 2003 17:06:50 +0000 (+0000) Subject: patch X-Git-Tag: V_0_4_3_4~13 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=c5dc22667edabecbd927a24495fee12bc823f387;p=helm.git patch --- 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) ->