From 270db4c9274496e65c16f16415b819b632a92f0b Mon Sep 17 00:00:00 2001 From: herbelin Date: Wed, 15 Oct 2003 13:39:47 +0000 Subject: Affichage = au lieu de == en v7 git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4642 85f007b7-540e-0410-9357-904b9bb8a0f7 --- theories/Reals/Rsyntax.v | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) (limited to 'theories/Reals') 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) ] -> [[ "``" (REXPR $n1) [1 0] "> "(REXPR $n2) "``" ]] | Req [ (eqT R $n1 $n2) ] -> - [[ "``" (REXPR $n1) [1 0] "== "(REXPR $n2)"``"]] + [[ "``" (REXPR $n1) [1 0] "= "(REXPR $n2)"``"]] | Rneq [ ~(eqT R $n1 $n2) ] -> [[ "``" (REXPR $n1) [1 0] "<> "(REXPR $n2) "``"]] | Rle_Rle [ (Rle $n1 $n2)/\(Rle $n2 $n3) ] -> -- cgit v1.2.3