Most warnings turned into errors and avoided

[helm.git] / matita / components / ng_extraction / ocaml.ml

diff --git a/matita/components/ng_extraction/ocaml.ml b/matita/components/ng_extraction/ocaml.ml
index a612c58d49be21fe889ae22165c1ee4c79f9faa5..213db1eb2be03409313e484424387c3e46a40851 100644 (file)
--- a/matita/components/ng_extraction/ocaml.ml
+++ b/matita/components/ng_extraction/ocaml.ml
@@ -115,7 +115,7 @@ let pp_fields status r fields =
 (*s Pretty-printing of types. [par] is a boolean indicating whether parentheses
     are needed or not. *)
 
-let rec pp_type status par vl t =
+let pp_type status par vl t =
   let rec pp_rec status par = function
     | Tmeta _ | Tvar' _ | Taxiom -> assert false
     | Tvar i -> (try status,pp_tvar (List.nth vl (pred i))
@@ -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
 
@@ -560,15 +560,16 @@ let pp_ind status co ind =
           status, pp_logical_ind p ++ res
        else
          let s = !init in
-          let status,res =
-           pp_one_ind
-             status prefix p.ip_vars names.(i) cnames.(i) p.ip_types in
-          let status,res2 = pp status (i+1) in
          begin
            init := (fnl () ++ str "and ");
-            status,
-           s ++
-           (if co then pp_coind p.ip_vars names.(i) else mt ()) ++ res ++ res2
+            let status,res =
+             pp_one_ind
+               status prefix p.ip_vars names.(i) cnames.(i) p.ip_types in
+            let status,res2 = pp status (i+1) in
+              status,
+             s ++
+             (if co then pp_coind p.ip_vars names.(i) else mt ()) ++
+              res ++ res2
          end
       end
   in