From 44b1f0c3a1e4bdc0abc3b02004c7b385ab63f7c5 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Thu, 20 Mar 2008 09:23:30 +0000 Subject: [PATCH] End of patch for computation of LetIn types. Now types of mutually (co)recursive function are added to the environment _after_ Implicit have been resolved. --- helm/software/components/cic/deannotate.ml | 16 ++++++++++------ 1 file changed, 10 insertions(+), 6 deletions(-) diff --git a/helm/software/components/cic/deannotate.ml b/helm/software/components/cic/deannotate.ml index ace1e6000..e81190842 100644 --- a/helm/software/components/cic/deannotate.ml +++ b/helm/software/components/cic/deannotate.ml @@ -164,6 +164,10 @@ let rec compute_letin_type context te = compute_letin_type context te, List.map (fun x -> compute_letin_type context x) pl) | C.Fix (fno,fl) -> + let fl = + List.map + (function (name,recno,ty,bo) -> + name,recno,compute_letin_type context ty, bo) fl in let tys,_ = List.fold_left (fun (types,len) (n,_,ty,_) -> @@ -174,11 +178,13 @@ let rec compute_letin_type context te = C.Fix (fno, List.map (fun (name,recno,ty,bo) -> - name, recno, - compute_letin_type context ty, - compute_letin_type (tys @ context) bo + name, recno, ty, compute_letin_type (tys @ context) bo ) fl) | C.CoFix (fno,fl) -> + let fl = + List.map + (function (name,ty,bo) -> + name, compute_letin_type context ty, bo) fl in let tys,_ = List.fold_left (fun (types,len) (n,ty,_) -> @@ -189,9 +195,7 @@ let rec compute_letin_type context te = C.CoFix (fno, List.map (fun (name,ty,bo) -> - name, - compute_letin_type context ty, - compute_letin_type (tys @ context) bo + name, ty, compute_letin_type (tys @ context) bo ) fl) ;; -- 2.39.2