X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Focaml%2Fcic_omdoc%2Feta_fixing.ml;h=9b20729103b37a0061d4f54a5b72cf4c9456b85a;hb=78cf601fd8b8dbb386b0db315dcbfdbe8256c15f;hp=24242b42675f34f4f4cdefaca68cdaa1a2f4a5d4;hpb=e626927b4c1c77bdcd6b545203a0a9c17a9ff136;p=helm.git

diff --git a/helm/ocaml/cic_omdoc/eta_fixing.ml b/helm/ocaml/cic_omdoc/eta_fixing.ml
index 24242b426..9b2072910 100644
--- a/helm/ocaml/cic_omdoc/eta_fixing.ml
+++ b/helm/ocaml/cic_omdoc/eta_fixing.ml
@@ -207,6 +207,11 @@ let eta_fix metasenv t =
        let l' =  List.map (eta_fix' context) l 
        in 
        (match l' with
+           [] -> assert false
+         | he::tl ->
+            let ty = CicTypeChecker.type_of_aux' metasenv context he in
+             fix_according_to_type ty he tl
+(*
          C.Const(uri,exp_named_subst)::l'' ->
            let constant_type =
              (match CicEnvironment.get_obj uri with
@@ -217,13 +222,7 @@ let eta_fix metasenv t =
              ) in 
            fix_according_to_type 
              constant_type (C.Const(uri,exp_named_subst)) l''
-(*
-           let result = fix_according_to_type constant_type (C.Const(uri,exp_named_subst)) l'' in
-           if not (CicReduction.are_convertible [] appl result) then 
-             (prerr_endline ("prima :" ^(CicPp.ppterm appl)); 
-              prerr_endline ("dopo :" ^(CicPp.ppterm result)));
-           result *)
-        | _ -> C.Appl l' )
+        | _ -> C.Appl l' *))
    | C.Const (uri,exp_named_subst) ->
        let exp_named_subst' =
        List.map