]> matita.cs.unibo.it Git - helm.git/commitdiff
Bug fixed: yet another case where tys of mutual recursive functions were not
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Wed, 14 Nov 2007 23:20:37 +0000 (23:20 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Wed, 14 Nov 2007 23:20:37 +0000 (23:20 +0000)
lifted correctly when pushed in the context.

helm/software/components/cic_exportation/cicExportation.ml

index 75088e6fc11fe7ab36573d9b3d55338e7cf704ad..8af058f9692d3bb8590fac15264d8236893c859b 100644 (file)
@@ -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