aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories
diff options
context:
space:
mode:
authorGravatar mayero <mayero@85f007b7-540e-0410-9357-904b9bb8a0f7>2000-12-15 22:12:20 +0000
committerGravatar mayero <mayero@85f007b7-540e-0410-9357-904b9bb8a0f7>2000-12-15 22:12:20 +0000
commit56a502cddb691c35857175574271d2992f44b4d1 (patch)
treefc2be639d534ddbc51ce1bb35d705935cd9710ee /theories
parent6dd5c4fb44f8c7cb7862d1b10a54bed3a2b809ed (diff)
pb niveau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1128 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories')
-rw-r--r--theories/Reals/Rsyntax.v7
1 files changed, 5 insertions, 2 deletions
diff --git a/theories/Reals/Rsyntax.v b/theories/Reals/Rsyntax.v
index 0685aaa9c..b30023643 100644
--- a/theories/Reals/Rsyntax.v
+++ b/theories/Reals/Rsyntax.v
@@ -163,14 +163,17 @@ Syntax constr
Rmult_inside
[<<(REXPR <<(Rmult $n1 $n2)>>)>>]
-> [ (REXPR $n1):E "*" [0 0] (REXPR $n2):L ]
- |Rdiv_inside
+(* |Rdiv_inside
[<<(REXPR <<(Rdiv $n1 $n2)>>)>>]
- -> [ (REXPR $n1):E "/" [0 0] (REXPR $n2):L ]
+ -> [ (REXPR $n1):E "/" [0 0] (REXPR $n2):L ]*)
;
level 5:
Ropp_inside [<<(REXPR <<(Ropp $n1)>>)>>] -> [ "-" (REXPR $n1):E ]
|Rinv_inside [<<(REXPR <<(Rinv $n1)>>)>>] -> [ "1""/" (REXPR $n1):E ]
+|Rdiv_inside
+ [<<(REXPR <<(Rdiv $n1 $n2)>>)>>]
+ -> [ (REXPR $n1):E "/" [0 0] (REXPR $n2):L ]
;
level 0: