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] *)
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
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