From 68d0e8729398bdb485670ed6d0e247af64d934fc Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen 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.2