Commit c403f5af authored by Guillaume Melquiond's avatar Guillaume Melquiond

Remove spurious newline at end of equivalence lemmas for Coq proofs.

parent 8e8e4595
...@@ -12,8 +12,6 @@ Lemma infix_lseq_def : forall (x:Z) (y:Z), (x <= y)%Z <-> ((x < y)%Z \/ ...@@ -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. exact Zle_lt_or_eq_iff.
Qed. Qed.
(* Why3 comment *) (* Why3 comment *)
(* infix_pl is replaced with (x + x1)%Z by the coq driver *) (* 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). ...@@ -92,7 +90,6 @@ Lemma infix_mn_def : forall (x:Z) (y:Z), ((x - y)%Z = (x + (-y)%Z)%Z).
reflexivity. reflexivity.
Qed. Qed.
(* Why3 goal *) (* Why3 goal *)
Lemma Comm1 : forall (x:Z) (y:Z), ((x * y)%Z = (y * x)%Z). Lemma Comm1 : forall (x:Z) (y:Z), ((x * y)%Z = (y * x)%Z).
Proof. Proof.
......
...@@ -12,8 +12,6 @@ Lemma infix_lseq_def : forall (x:R) (y:R), (x <= y)%R <-> ((x < y)%R \/ ...@@ -12,8 +12,6 @@ Lemma infix_lseq_def : forall (x:R) (y:R), (x <= y)%R <-> ((x < y)%R \/
reflexivity. reflexivity.
Qed. Qed.
(* Why3 comment *) (* Why3 comment *)
(* infix_pl is replaced with (x + x1)%R by the coq driver *) (* 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). ...@@ -88,8 +86,6 @@ Lemma infix_mn_def : forall (x:R) (y:R), ((x - y)%R = (x + (-y)%R)%R).
reflexivity. reflexivity.
Qed. Qed.
(* Why3 goal *) (* Why3 goal *)
Lemma Comm1 : forall (x:R) (y:R), ((x * y)%R = (y * x)%R). Lemma Comm1 : forall (x:R) (y:R), ((x * y)%R = (y * x)%R).
Proof. Proof.
...@@ -122,7 +118,6 @@ Lemma infix_sl_def : forall (x:R) (y:R), ((Rdiv x y)%R = (x * (Rinv y))%R). ...@@ -122,7 +118,6 @@ Lemma infix_sl_def : forall (x:R) (y:R), ((Rdiv x y)%R = (x * (Rinv y))%R).
reflexivity. reflexivity.
Qed. Qed.
(* Why3 goal *) (* Why3 goal *)
Lemma add_div : forall (x:R) (y:R) (z:R), (~ (z = 0%R)) -> 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). ((Rdiv (x + y)%R z)%R = ((Rdiv x z)%R + (Rdiv y z)%R)%R).
......
...@@ -10,8 +10,6 @@ Lemma sqr_def : forall (x:R), ((Rsqr x) = (x * x)%R). ...@@ -10,8 +10,6 @@ Lemma sqr_def : forall (x:R), ((Rsqr x) = (x * x)%R).
reflexivity. reflexivity.
Qed. Qed.
(* Why3 comment *) (* Why3 comment *)
(* sqrt is replaced with (sqrt x) by the coq driver *) (* sqrt is replaced with (sqrt x) by the coq driver *)
......
...@@ -778,8 +778,7 @@ let print_equivalence_lemma ~prev info fmt name (ls,ld) = ...@@ -778,8 +778,7 @@ let print_equivalence_lemma ~prev info fmt name (ls,ld) =
print_ne_params all_ty_params print_ne_params all_ty_params
(print_expr info) def_formula; (print_expr info) def_formula;
fprintf fmt "%a@\n" fprintf fmt "%a@\n"
(print_previous_proof (Some (all_ty_params,def_formula)) info) prev; (print_previous_proof (Some (all_ty_params,def_formula)) info) prev
fprintf fmt "@\n"
let print_equivalence_lemma ~old info fmt ((ls,_) as d) = let print_equivalence_lemma ~old info fmt ((ls,_) as d) =
if info.realization && (Mid.mem ls.ls_name info.info_syn) then 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) = ...@@ -788,7 +787,6 @@ let print_equivalence_lemma ~old info fmt ((ls,_) as d) =
let prev = output_till_statement fmt old name in let prev = output_till_statement fmt old name in
(print_equivalence_lemma ~prev info fmt name d; forget_tvs ()) (print_equivalence_lemma ~prev info fmt name d; forget_tvs ())
let print_logic_decl ~old info fmt d = let print_logic_decl ~old info fmt d =
(** During realization the definition of a "builtin" symbol is (** During realization the definition of a "builtin" symbol is
printed and an equivalence lemma with associated coq function is printed and an equivalence lemma with associated coq function is
......
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