From: Claudio Sacerdoti Coen Date: Wed, 14 Nov 2007 23:20:37 +0000 (+0000) Subject: Bug fixed: yet another case where tys of mutual recursive functions were not X-Git-Tag: make_still_working~5851 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=4bc8832972166cc497cd8dc23faa6b63124c2d0b;p=helm.git Bug fixed: yet another case where tys of mutual recursive functions were not lifted correctly when pushed in the context. --- diff --git a/helm/software/components/cic_exportation/cicExportation.ml b/helm/software/components/cic_exportation/cicExportation.ml index 75088e6fc..8af058f96 100644 --- a/helm/software/components/cic_exportation/cicExportation.ml +++ b/helm/software/components/cic_exportation/cicExportation.ml @@ -335,11 +335,12 @@ let rec pp ~in_type t context = ) connames_and_argsno_and_patterns)) ^ ")\n"))) | C.Fix (no, funs) -> - let names = - List.rev - (List.map - (function (name,_,ty,_) -> - Some (C.Name name,Cic.Decl ty)) funs) + let names,_ = + List.fold_left + (fun (types,len) (n,_,ty,_) -> + (Some (C.Name n,(C.Decl (CicSubstitution.lift len ty)))::types, + len+1) + ) ([],0) funs in "let rec " ^ List.fold_right @@ -351,11 +352,12 @@ let rec pp ~in_type t context = Some (Cic.Name n,_) -> n | _ -> assert false) | C.CoFix (no,funs) -> - let names = - List.rev - (List.map - (function (name,ty,_) -> - Some (C.Name name,Cic.Decl ty)) funs) + let names,_ = + List.fold_left + (fun (types,len) (n,ty,_) -> + (Some (C.Name n,(C.Decl (CicSubstitution.lift len ty)))::types, + len+1) + ) ([],0) funs in "\nCoFix " ^ " {" ^ List.fold_right