From 0316891a0eeb8d88cd5cc225fd4bb18e3583a271 Mon Sep 17 00:00:00 2001
From: mayero
Date: Mon, 4 Jun 2001 12:32:39 +0000
Subject: Correction bug outside

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1778 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 theories/Reals/Rsyntax.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/theories/Reals/Rsyntax.v b/theories/Reals/Rsyntax.v
index 4afaa83ac2..9a14dae65f 100644
--- a/theories/Reals/Rsyntax.v
+++ b/theories/Reals/Rsyntax.v
@@ -110,7 +110,7 @@ Syntax constr
   level 7:
     Rplus [ (Rplus $n1 $n2) ]
       -> [ [<hov 0> "``"(REXPR $n1):E "+"  [0 0] (REXPR $n2):L "``"] ]
-   | Rconst [(Rplus $r R1)] -> [$r:"r_printer_outside"]
+   | Rconst [(Rplus R1 $r)] -> [$r:"r_printer_outside"]
    | Rminus [ (Rminus $n1 $n2) ]
       -> [ [<hov 0> "``"(REXPR $n1):E "-" [0 0] (REXPR $n2):L "``"] ]
   ;
-- 
cgit v1.2.3