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

diff --git a/matita/components/ng_extraction/ocaml.ml b/matita/components/ng_extraction/ocaml.ml
index 001845e35..213db1eb2 100644
--- 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))
@@ -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