]> matita.cs.unibo.it Git - helm.git/commitdiff
Reindentation
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Tue, 23 Sep 2003 15:58:28 +0000 (15:58 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Tue, 23 Sep 2003 15:58:28 +0000 (15:58 +0000)
helm/ocaml/cic_omdoc/eta_fixing.ml

index d6293d2434ad61af36b7c94203a0cf7b6c8641c7..4a529a2bc54c536e873075d0715e209ba082aabc 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 = 
-              CicTypeChecker.type_of_aux' metasenv context term in
+                let term_type = 
+            TypeInference.type_of_aux' metasenv context term
+           in
             (match term_type with
                C.Appl (hd::params) -> 
                  List.map (fun (_,t) -> clean_up t params) constructors