Commit 60b61466 authored by Guillaume Melquiond's avatar Guillaume Melquiond

Avoid some spurious blank lines in the Coq printer.

parent c7756ed4
......@@ -58,4 +58,3 @@ Proof.
now intros [|] [|].
Qed.
......@@ -178,4 +178,3 @@ Definition lt (x:floating_point.DoubleFormat.double)
Definition gt (x:floating_point.DoubleFormat.double)
(y:floating_point.DoubleFormat.double): Prop := ((value y) < (value x))%R.
......@@ -10,7 +10,6 @@ Definition double : Type.
exact (t 53 1024).
Defined.
Global Instance double_WhyType : WhyType double.
Proof.
apply t_WhyType.
......
......@@ -13,4 +13,3 @@ Inductive mode :=
Axiom mode_WhyType : WhyType mode.
Existing Instance mode_WhyType.
......@@ -189,4 +189,3 @@ Definition lt (x:floating_point.SingleFormat.single)
Definition gt (x:floating_point.SingleFormat.single)
(y:floating_point.SingleFormat.single): Prop := ((value y) < (value x))%R.
......@@ -10,7 +10,6 @@ Definition single : Type.
exact (t 24 128).
Defined.
Global Instance single_WhyType : WhyType single.
Proof.
apply t_WhyType.
......
......@@ -33,4 +33,3 @@ Lemma Abs_pos : forall (x:Z), (0%Z <= (Zabs x))%Z.
exact Zabs_pos.
Qed.
......@@ -141,4 +141,3 @@ apply Zmult_le_0_compat with (1 := Hy).
now apply Zlt_le_weak.
Qed.
......@@ -18,4 +18,3 @@ simpl in H1.
omega.
Qed.
......@@ -191,4 +191,3 @@ ring.
auto with zarith.
Qed.
......@@ -112,5 +112,4 @@ rewrite IHn.
now rewrite Assoc, <- (Assoc y), (Comm y), 2!Assoc.
Qed.
End Exponentiation.
......@@ -160,4 +160,3 @@ Proof.
exact Zmult_le_compat_r.
Qed.
......@@ -78,4 +78,3 @@ intros x y _.
apply Zmin_comm.
Qed.
......@@ -79,4 +79,3 @@ rewrite 3!power_is_exponentiation ; auto with zarith.
apply Power_mult2 ; auto with zarith.
Qed.
......@@ -82,4 +82,3 @@ apply in_split.
now apply Mem.mem_std.
Qed.
......@@ -19,4 +19,3 @@ Definition tl {a:Type} {a_WT:WhyType a} (l:(list a)): (option (list a)) :=
| (cons _ t) => (Some t)
end.
......@@ -44,4 +44,3 @@ generalize (Length_nonnegative t).
omega.
Qed.
......@@ -3,9 +3,6 @@
Require Import BuiltIn.
Require BuiltIn.
Global Instance list_WhyType : forall T {T_WT : WhyType T}, WhyType (list T).
split.
apply nil.
......
......@@ -11,7 +11,6 @@ Fixpoint mem {a:Type} {a_WT:WhyType a} (x:a) (l:(list a)) {struct l}: Prop :=
| (cons y r) => (x = y) \/ (mem x r)
end.
Lemma mem_std :
forall {a:Type} {a_WT:WhyType a} (x:a) (l:list a),
mem x l <-> List.In x l.
......
......@@ -34,4 +34,3 @@ generalize (Zeq_bool_if n 0).
now case Zeq_bool.
Qed.
......@@ -36,4 +36,3 @@ Proof.
now intros a a_WT [|h t].
Qed.
......@@ -70,4 +70,3 @@ specialize (IHq _ H).
omega.
Qed.
......@@ -57,4 +57,3 @@ apply IHl1.
omega.
Qed.
......@@ -45,4 +45,3 @@ rewrite 2!Length.length_std.
now rewrite List.rev_length.
Qed.
......@@ -77,4 +77,3 @@ Proof.
easy.
Qed.
......@@ -137,4 +137,3 @@ now apply sym_eq, H1 ; split.
now apply H1 ; split.
Qed.
......@@ -217,4 +217,3 @@ now apply -> even_divides.
exact H0.
Qed.
......@@ -149,4 +149,3 @@ apply Zis_gcd_mult.
apply Zgcd_is_gcd.
Qed.
......@@ -112,4 +112,3 @@ intros k.
now exists k.
Qed.
......@@ -180,4 +180,3 @@ apply Pp.
omega.
Qed.
......@@ -3,9 +3,6 @@
Require Import BuiltIn.
Require BuiltIn.
Global Instance option_WhyType : forall T {T_WT : WhyType T}, WhyType (option T).
split.
apply @None.
......
......@@ -69,4 +69,3 @@ replace (x - z)%R with ((x - y) + (y - z))%R by ring.
apply Rabs_triang.
Qed.
......@@ -53,4 +53,3 @@ Definition log2 (x:R): R := (Rdiv (ln x) (ln 2%R))%R.
(* Why3 assumption *)
Definition log10 (x:R): R := (Rdiv (ln x) (ln 10%R))%R.
......@@ -38,4 +38,3 @@ Lemma Neg : forall (x:Z), ((IZR (-x)%Z) = (-(IZR x))%R).
exact opp_IZR.
Qed.
......@@ -54,4 +54,3 @@ apply Rmin_right.
now apply Rlt_le.
Qed.
......@@ -102,4 +102,3 @@ replace 1%R with (1*1)%R by auto with real.
apply Rmult_le_compat; auto with real.
Qed.
......@@ -223,4 +223,3 @@ intros x y z H Zz.
now apply Rmult_le_compat_r.
Qed.
......@@ -4,4 +4,3 @@ Require Import BuiltIn.
Require BuiltIn.
Require real.Real.
......@@ -42,4 +42,3 @@ intros x y (h1 & h2); apply sqrt_le_1; auto.
apply Rle_trans with x; auto.
Qed.
......@@ -235,4 +235,3 @@ intros a a_WT x.
now unfold all.
Qed.
......@@ -960,7 +960,7 @@ let print_decl ~old info fmt d =
print_prop_decl ~prev info fmt pr
let print_decls ~old info fmt dl =
fprintf fmt "@\n@[<hov>%a@\n@]" (print_list nothing (print_decl ~old info)) dl
fprintf fmt "@\n@[<hov>%a@]" (print_list nothing (print_decl ~old info)) dl
let print_task printer_args realize ?old fmt task =
(* eprintf "Task:%a@.@." Pretty.print_task task; *)
......
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