From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
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