diff options
| -rw-r--r-- | theories/Reals/SplitAbsolu.v | 2 | ||||
| -rw-r--r-- | theories/Reals/SplitRmult.v | 2 |
2 files changed, 2 insertions, 2 deletions
diff --git a/theories/Reals/SplitAbsolu.v b/theories/Reals/SplitAbsolu.v index ba2fbf535..19c9e49a6 100644 --- a/theories/Reals/SplitAbsolu.v +++ b/theories/Reals/SplitAbsolu.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (***********************************************************************) -(* $Id$ *) +(*i $Id$ i*) Require Export Rbasic_fun. diff --git a/theories/Reals/SplitRmult.v b/theories/Reals/SplitRmult.v index 479112326..217b26bbc 100644 --- a/theories/Reals/SplitRmult.v +++ b/theories/Reals/SplitRmult.v @@ -8,7 +8,7 @@ (*i $Id$ i*) -(*Lemma mult_non_zero :(r1,r2:R)``r1<>0`` /\ ``r2<>0`` -> ``r1*r2<>0``.*) +(*i Lemma mult_non_zero :(r1,r2:R)``r1<>0`` /\ ``r2<>0`` -> ``r1*r2<>0``. i*) Require Rbase. |