*** empty log message ***

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1197 85f007b7-540e-0410-9357-904b9bb8a0f7

2 files changed, 12 insertions, 1 deletions

diff --git a/parsing/g_rsyntax.ml b/parsing/g_rsyntax.ml
index d4e56c86b8..03f9fcbc64 100644
--- a/parsing/g_rsyntax.ml
+++ b/parsing/g_rsyntax.ml
@@ -65,6 +65,17 @@ let r_printer std_pr p =
     | Some i -> [< 'sTR (string_of_int (i+1)) >]
     | None -> std_pr (replace_plus p)
 
+let r_printer_outside std_pr p =
+ let (_,ast1,astp,_) = get_r_sign dummy_loc in
+  match (int_of_r p) with
+    | Some i -> [< 'sTR "``"; 'sTR (string_of_int (i+1)); 'sTR "``" >]
+    | None -> std_pr (replace_plus p)
 
 let _ = Esyntax.Ppprim.add ("r_printer", r_printer)
+let _ = Esyntax.Ppprim.add ("r_printer_outside", r_printer_outside)
+
+
+
+
+
 
diff --git a/theories/Reals/Rsyntax.v b/theories/Reals/Rsyntax.v
index b30023643c..4647a1250b 100644
--- a/theories/Reals/Rsyntax.v
+++ b/theories/Reals/Rsyntax.v
@@ -98,12 +98,12 @@ Syntax constr
                                 [1 0] "< " (REXPR $n3) "``"]]
   | Rzero [ R0 ] -> ["``0``"]
   | Rone [ R1 ] -> ["``1``"]
-  | Rconst [(Rplus $r R1)] -> [$r:"r_printer"]
   ;
 
   level 7:
     Rplus [ (Rplus $n1 $n2) ]
       -> [ [<hov 0> "``"(REXPR $n1):E "+"  [0 0] (REXPR $n2):L "``"] ]
+   | Rconst [(Rplus $r R1)] -> [$r:"r_printer_outside"]
    | Rminus [ (Rminus $n1 $n2) ]
       -> [ [<hov 0> "``"(REXPR $n1):E "-" [0 0] (REXPR $n2):L "``"] ]
   ;