]> matita.cs.unibo.it Git - helm.git/commitdiff
Slightly nicer output.
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Mon, 5 Nov 2007 12:18:15 +0000 (12:18 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Mon, 5 Nov 2007 12:18:15 +0000 (12:18 +0000)
helm/software/components/cic_exportation/cicExportation.ml

index 7297dd56a8fb2ce375f087077d348532cfac4826..dbb7194a998e69ade2bd60d166712e39754e449f 100644 (file)
@@ -269,7 +269,7 @@ let rec pp t context =
                 in
                  combine (connames_and_argsno,patterns)
                in
-                "\n(match " ^ pp te context ^ " with \n" ^
+                "\n(match " ^ pp te context ^ " with \n   " ^
                  (String.concat "\n | "
                   (List.map
                    (fun (x,argsno,y) ->
@@ -308,7 +308,7 @@ let rec pp t context =
            (function (name,_,ty,_) ->
              Some (C.Name name,Cic.Decl ty)) funs)
        in
-         "\nlet rec " ^
+         "let rec " ^
          List.fold_right
           (fun (name,ind,ty,bo) i -> name ^ " = \n" ^
             pp bo (names@context) ^ i)
@@ -316,7 +316,7 @@ let rec pp t context =
          " in " ^
          (match get_nth names (no + 1) with
              Some (Cic.Name n,_) -> n
-           | _ -> assert false) ^ "\n"
+           | _ -> assert false)
     | C.CoFix (no,funs) ->
        let names =
         List.rev