Commit 4a8c0479 authored by Guillaume Melquiond's avatar Guillaume Melquiond
Browse files

Fix missing blank line.

parent 6181e14e
......@@ -543,7 +543,7 @@ let print_type_decl ~old info fmt (ts,def) =
| Some (Query (_,Notation,c)) ->
fprintf fmt "(* Why3 goal *)@\n%s@\n" c
| _ ->
fprintf fmt "(* Why3 goal *)@\n@[<hov 2>Definition %s : %aType.@]@\n%a"
fprintf fmt "(* Why3 goal *)@\n@[<hov 2>Definition %s : %aType.@]@\n%a@\n"
name print_params_list ts.ts_args
(print_previous_proof true) prev
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment