diff options
| author | Xavier Leroy <xavier.leroy@college-de-france.fr> | 2019-04-04 18:46:55 +0200 |
|---|---|---|
| committer | Xavier Leroy <xavier.leroy@college-de-france.fr> | 2019-04-04 18:46:55 +0200 |
| commit | 7361c01f5df99e36f700b8257115fc96f2fff779 (patch) | |
| tree | dbae0764f2ecf1ee54b21d513c7d4b3239c23497 | |
| parent | 7644d49d591799902f50c2240900db4f302ceff5 (diff) | |
| download | compcert-7361c01f5df99e36f700b8257115fc96f2fff779.tar.gz compcert-7361c01f5df99e36f700b8257115fc96f2fff779.zip | |
Floats.v: remove leftover Print commands
These were committed by mistake.
| -rw-r--r-- | lib/Floats.v | 6 |
1 files changed, 1 insertions, 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. |