From 7361c01f5df99e36f700b8257115fc96f2fff779 Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Thu, 4 Apr 2019 18:46:55 +0200 Subject: Floats.v: remove leftover Print commands These were committed by mistake. --- lib/Floats.v | 6 +----- 1 file changed, 1 insertion(+), 5 deletions(-) diff --git a/lib/Floats.v b/lib/Floats.v index ece9ea18..3ce8f4b4 100644 --- a/lib/Floats.v +++ b/lib/Floats.v @@ -101,7 +101,7 @@ Lemma digits2_log2: Proof. assert (E: forall p, Digits.digits2_pos p = Pos.size p). { induction p; simpl; rewrite ?IHp; auto. } - intros p. rewrite E. + intros p. rewrite E. destruct p; simpl; rewrite ?Pos.add_1_r; reflexivity. Qed. @@ -110,10 +110,6 @@ Local Notation __ := (eq_refl Datatypes.Lt). Local Hint Extern 1 (Prec_gt_0 _) => exact (eq_refl Datatypes.Lt). Local Hint Extern 1 (_ < _) => exact (eq_refl Datatypes.Lt). -Print Digits.digits2_pos. -Print Pos.size. - - (** * Double-precision FP numbers *) Module Float. -- cgit