3 files changed, 9 insertions, 6 deletions
diff --git a/theories/Reals/Rbase.v b/theories/Reals/Rbase.v
index 898783cbc8..4b4ab63514 100644
--- a/theories/Reals/Rbase.v
+++ b/theories/Reals/Rbase.v
@@ -286,13 +286,14 @@ Lemma Rplus_Ropp:(x,y:R)``x+y==0``->``y== -x``.
   | Ring ].
 Save.
 
-(* New *)
+(*i New i*)
 Hint eqT_R_congr : real := Resolve (congr_eqT R).
 
 Lemma Rplus_plus_r:(r,r1,r2:R)(r1==r2)->``r+r1==r+r2``.
   Auto with real.
 Save.
-(* Old *) Hints Resolve Rplus_plus_r : v62.
+
+(*i Old i*)Hints Resolve Rplus_plus_r : v62.
 
 (**********)
 Lemma r_Rplus_plus:(r,r1,r2:R)``r+r1==r+r2``->r1==r2.
@@ -358,7 +359,8 @@ Hints Resolve Rmult_1r : real.
 Lemma Rmult_mult_r:(r,r1,r2:R)r1==r2->``r*r1==r*r2``.
   Auto with real.
 Save.
-(* OLD *) Hints Resolve Rmult_mult_r : v62.
+
+(*i OLD i*)Hints Resolve Rmult_mult_r : v62.
 
 (**********)
 Lemma r_Rmult_mult:(r,r1,r2:R)(``r*r1==r*r2``)->``r<>0``->(r1==r2).
diff --git a/theories/Reals/Rdefinitions.v b/theories/Reals/Rdefinitions.v
index 1bd1e5ec7d..b5ac6e1f9c 100644
--- a/theories/Reals/Rdefinitions.v
+++ b/theories/Reals/Rdefinitions.v
@@ -25,7 +25,8 @@ Parameter Ropp:R->R.
 Parameter Rinv:R->R. 
 Parameter Rlt:R->R->Prop.    
 Parameter up:R->Z.
-(*********************************************************)
+
+(*i*******************************************************i*)
 
 (**********)
 Definition Rgt:R->R->Prop:=[r1,r2:R](Rlt r2 r1).
diff --git a/theories/Reals/Rsyntax.v b/theories/Reals/Rsyntax.v
index 4f4899f402..b8eef3a253 100644
--- a/theories/Reals/Rsyntax.v
+++ b/theories/Reals/Rsyntax.v
@@ -71,9 +71,9 @@ Grammar command command0 :=
 Grammar command atomic_pattern :=
   r_in_pattern [ "``" rnatural:rnumber($c) "``" ] -> [$c].   
 
-(** pp **)
+(*i* pp **)
 (* pb: on rajoute des () lorsque les constantes terminent par 1 lors de
-l'appel avec NRplus *)
+l'appel avec NRplus i*)