]> matita.cs.unibo.it Git - helm.git/commitdiff
patch
authorFerruccio Guidi <ferruccio.guidi@unibo.it>
Tue, 23 Sep 2003 17:06:50 +0000 (17:06 +0000)
committerFerruccio Guidi <ferruccio.guidi@unibo.it>
Tue, 23 Sep 2003 17:06:50 +0000 (17:06 +0000)
helm/ocaml/cic_omdoc/eta_fixing.ml

index 4a529a2bc54c536e873075d0715e209ba082aabc..c224bcf65ad1fb25b7c36d6739ccd996ff94e644 100644 (file)
@@ -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) ->