diff --git a/lib/coq/int/Int.v b/lib/coq/int/Int.v
index 2c85a13eba7b66a09a6c1f132ed73a61886b9878..b8c3a5699f1e598babe2406b49a32643d86c3292 100644
--- a/lib/coq/int/Int.v
+++ b/lib/coq/int/Int.v
@@ -12,8 +12,6 @@ Lemma infix_lseq_def : forall (x:Z) (y:Z), (x <= y)%Z <-> ((x < y)%Z \/
 exact Zle_lt_or_eq_iff.
 Qed.
 
-
-
 (* Why3 comment *)
 (* infix_pl is replaced with (x + x1)%Z by the coq driver *)
 
@@ -92,7 +90,6 @@ Lemma infix_mn_def : forall (x:Z) (y:Z), ((x - y)%Z = (x + (-y)%Z)%Z).
 reflexivity.
 Qed.
 
-
 (* Why3 goal *)
 Lemma Comm1 : forall (x:Z) (y:Z), ((x * y)%Z = (y * x)%Z).
 Proof.
diff --git a/lib/coq/real/Real.v b/lib/coq/real/Real.v
index 6f8eb07ce4daade4eb12ce71af5b4231b865c074..2d60a0a2288bf0b2dcd8f939c67d143feffcdb66 100644
--- a/lib/coq/real/Real.v
+++ b/lib/coq/real/Real.v
@@ -12,8 +12,6 @@ Lemma infix_lseq_def : forall (x:R) (y:R), (x <= y)%R <-> ((x < y)%R \/
 reflexivity.
 Qed.
 
-
-
 (* Why3 comment *)
 (* infix_pl is replaced with (x + x1)%R by the coq driver *)
 
@@ -88,8 +86,6 @@ Lemma infix_mn_def : forall (x:R) (y:R), ((x - y)%R = (x + (-y)%R)%R).
 reflexivity.
 Qed.
 
-
-
 (* Why3 goal *)
 Lemma Comm1 : forall (x:R) (y:R), ((x * y)%R = (y * x)%R).
 Proof.
@@ -122,7 +118,6 @@ Lemma infix_sl_def : forall (x:R) (y:R), ((Rdiv x y)%R = (x * (Rinv y))%R).
 reflexivity.
 Qed.
 
-
 (* Why3 goal *)
 Lemma add_div : forall (x:R) (y:R) (z:R), (~ (z = 0%R)) ->
   ((Rdiv (x + y)%R z)%R = ((Rdiv x z)%R + (Rdiv y z)%R)%R).
diff --git a/lib/coq/real/Square.v b/lib/coq/real/Square.v
index 9c088ef6b2cbc58c77566766cc335d212bc67ed7..8de1a83660f2bc99dbc1ed27cd463efc015a37ca 100644
--- a/lib/coq/real/Square.v
+++ b/lib/coq/real/Square.v
@@ -10,8 +10,6 @@ Lemma sqr_def : forall (x:R), ((Rsqr x) = (x * x)%R).
 reflexivity.
 Qed.
 
-
-
 (* Why3 comment *)
 (* sqrt is replaced with (sqrt x) by the coq driver *)
 
diff --git a/src/printer/coq.ml b/src/printer/coq.ml
index bf8328b2b260f5be094e699f7ca5dadb0385967a..b344bef0c843365203a2bedf337dec3aefb3c341 100644
--- a/src/printer/coq.ml
+++ b/src/printer/coq.ml
@@ -778,8 +778,7 @@ let print_equivalence_lemma ~prev info fmt name (ls,ld) =
     print_ne_params all_ty_params
     (print_expr info) def_formula;
   fprintf fmt "%a@\n"
-    (print_previous_proof (Some (all_ty_params,def_formula)) info) prev;
-  fprintf fmt "@\n"
+    (print_previous_proof (Some (all_ty_params,def_formula)) info) prev
 
 let print_equivalence_lemma ~old info fmt ((ls,_) as d) =
   if info.realization && (Mid.mem ls.ls_name info.info_syn) then
@@ -788,7 +787,6 @@ let print_equivalence_lemma ~old info fmt ((ls,_) as d) =
     let prev = output_till_statement fmt old name in
     (print_equivalence_lemma ~prev info fmt name d; forget_tvs ())
 
-
 let print_logic_decl ~old info fmt d =
   (** During realization the definition of a "builtin" symbol is
       printed and an equivalence lemma with associated coq function is