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 24242b42675f34f4f4cdefaca68cdaa1a2f4a5d4..9b20729103b37a0061d4f54a5b72cf4c9456b85a 100644 (file)
--- 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