From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Tue, 10 Feb 2004 12:11:36 +0000 (+0000)
Subject: Only applications whose head was a constant were eta-fixed.
X-Git-Tag: V_0_3_0~38
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=68d0e8729398bdb485670ed6d0e247af64d934fc;p=helm.git

Only applications whose head was a constant were eta-fixed.
Result: sometimes the generated term was no longer well-typed.
The fix consists in calling the type-checker on the head of the
applications. Slower, but more reliable.
---

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