diff options
| author | herbelin | 2003-10-15 13:39:47 +0000 |
|---|---|---|
| committer | herbelin | 2003-10-15 13:39:47 +0000 |
| commit | 270db4c9274496e65c16f16415b819b632a92f0b (patch) | |
| tree | d5f1c9e71247b52566bc2b369955b0d6cd8d9740 /theories/Reals | |
| parent | 2104447c823a67bb5fea36957bfec5f271394bf2 (diff) | |
Affichage = au lieu de == en v7
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4642 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/Reals')
| -rw-r--r-- | theories/Reals/Rsyntax.v | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/theories/Reals/Rsyntax.v b/theories/Reals/Rsyntax.v index cf0d8ca46e..95d60efebe 100644 --- a/theories/Reals/Rsyntax.v +++ b/theories/Reals/Rsyntax.v @@ -25,6 +25,7 @@ with rformula : constr := form_expr [ rexpr($p) ] -> [ $p ] (* | form_eq [ rexpr($p) "==" rexpr($c) ] -> [ (eqT R $p $c) ] *) | form_eq [ rexpr($p) "==" rexpr($c) ] -> [ (eqT ? $p $c) ] +| form_eq2 [ rexpr($p) "=" rexpr($c) ] -> [ (eqT ? $p $c) ] | form_le [ rexpr($p) "<=" rexpr($c) ] -> [ (Rle $p $c) ] | form_lt [ rexpr($p) "<" rexpr($c) ] -> [ (Rlt $p $c) ] | form_ge [ rexpr($p) ">=" rexpr($c) ] -> [ (Rge $p $c) ] @@ -99,7 +100,7 @@ Syntax constr | Rgt [ (Rgt $n1 $n2) ] -> [[<hov 0> "``" (REXPR $n1) [1 0] "> "(REXPR $n2) "``" ]] | Req [ (eqT R $n1 $n2) ] -> - [[<hov 0> "``" (REXPR $n1) [1 0] "== "(REXPR $n2)"``"]] + [[<hov 0> "``" (REXPR $n1) [1 0] "= "(REXPR $n2)"``"]] | Rneq [ ~(eqT R $n1 $n2) ] -> [[<hov 0> "``" (REXPR $n1) [1 0] "<> "(REXPR $n2) "``"]] | Rle_Rle [ (Rle $n1 $n2)/\(Rle $n2 $n3) ] -> |