X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fcomponents%2Fng_extraction%2Focaml.ml;h=001845e35e046eb449ca8c4554d874c2701be0f5;hb=59dfa0b85ba8a74f4b5c175f72ac7ebeed6fca7f;hp=a612c58d49be21fe889ae22165c1ee4c79f9faa5;hpb=18c1584b94ad85301a95b69fe0a8fa8e02b61648;p=helm.git

diff --git a/matita/components/ng_extraction/ocaml.ml b/matita/components/ng_extraction/ocaml.ml
index a612c58d4..001845e35 100644
--- a/matita/components/ng_extraction/ocaml.ml
+++ b/matita/components/ng_extraction/ocaml.ml
@@ -438,7 +438,7 @@ and pp_fix status par env i (ids,bl) args =
 let pp_val status e typ =
  let status,res = pp_type status false [] typ in
   status,
-  hov 4 (str "(** val " ++ e ++ str " :" ++ spc ()++res++ str " **)") ++ fnl2 ()
+  hov 4 (str "(** val " ++ e ++ str " :" ++ spc ()++res++ str " **)") ++ fnl ()
 
 (*s Pretty-printing of [Dfix] *)
 
@@ -461,7 +461,7 @@ let pp_Dfix status (rv,c,t) =
         let status,res = pp_val status names.(i) t.(i) in
         let status,res2 = pp status false (i+1) in
         status,
-	(if init then mt () else fnl2 ()) ++ res ++
+	(if init then mt () else fnl ()) ++ res ++
 	str (if init then "let rec " else "and ") ++ names.(i) ++ def ++ res2
   in pp status true 0