diff options
Diffstat (limited to 'theories/Reals/R_Ifp.v')
| -rw-r--r-- | theories/Reals/R_Ifp.v | 12 |
1 files changed, 6 insertions, 6 deletions
diff --git a/theories/Reals/R_Ifp.v b/theories/Reals/R_Ifp.v index 240b8c920..1f6abb175 100644 --- a/theories/Reals/R_Ifp.v +++ b/theories/Reals/R_Ifp.v @@ -8,16 +8,16 @@ (*i $Id$ i*) -(*********************************************************) -(* Complements for the reals.Integer and fractional part *) -(* *) -(*********************************************************) +(**********************************************************) +(** Complements for the reals.Integer and fractional part *) +(* *) +(**********************************************************) Require Export Rbase. Require Omega. (*********************************************************) -(* Fractional part *) +(** Fractional part *) (*********************************************************) (**********) @@ -101,7 +101,7 @@ Elim (for_base_fp r);Intros;Rewrite <-Ropp_O; Save. (*********************************************************) -(* Properties *) +(** Properties *) (*********************************************************) (**********) |