From 68d0e8729398bdb485670ed6d0e247af64d934fc Mon Sep 17 00:00:00 2001
From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Tue, 10 Feb 2004 12:11:36 +0000
Subject: [PATCH] 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.
---
helm/ocaml/cic_omdoc/eta_fixing.ml | 13 ++++++-------
1 file changed, 6 insertions(+), 7 deletions(-)
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
--
2.39.5