X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=components%2Fcic_exportation%2FcicExportation.ml;fp=components%2Fcic_exportation%2FcicExportation.ml;h=8af058f9692d3bb8590fac15264d8236893c859b;hb=1d6910f6ee5dfd0e53fcec8c020311baba922a4c;hp=75088e6fc11fe7ab36573d9b3d55338e7cf704ad;hpb=3e4f0587ac2f1136c4f8314e8e2f8447fe4743e6;p=helm.git

diff --git a/components/cic_exportation/cicExportation.ml b/components/cic_exportation/cicExportation.ml
index 75088e6fc..8af058f96 100644
--- a/components/cic_exportation/cicExportation.ml
+++ b/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