From dda304e136bc43aae6714dc773aaa48330716ba9 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Wed, 14 May 2003 00:14:06 +0000
Subject: Suppression de 'R' dans la notation == entre

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4015 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 theories/Reals/Exp_prop.v | 2 +-
 theories/Reals/Rsyntax.v  | 9 +++++++--
 2 files changed, 8 insertions(+), 3 deletions(-)

diff --git a/theories/Reals/Exp_prop.v b/theories/Reals/Exp_prop.v
index a180c4a5b9..5c06af34a4 100644
--- a/theories/Reals/Exp_prop.v
+++ b/theories/Reals/Exp_prop.v
@@ -805,7 +805,7 @@ Apply pow_maj_Rabs.
 Rewrite Rabsolu_Rabsolu; Left; Apply H1.
 Apply Rle_sym1; Left; Apply Rlt_Rinv; Apply H2.
 Apply INR_fact_lt_0.
-Cut ``r<>0``.
+Cut (r::R)<>``0``.
 Intro; Apply Alembert_C2.
 Intro; Apply Rabsolu_no_R0.
 Unfold Rdiv; Apply prod_neq_R0.
diff --git a/theories/Reals/Rsyntax.v b/theories/Reals/Rsyntax.v
index 4733ad3cb8..a008cd06ec 100644
--- a/theories/Reals/Rsyntax.v
+++ b/theories/Reals/Rsyntax.v
@@ -23,13 +23,18 @@ with rnumber :=
 
 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 R $p $c) ] *)
+| form_eq [ 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) ]
 | form_gt [ rexpr($p) ">" rexpr($c) ] -> [ (Rgt $p $c) ]
+(*
 | form_eq_eq [ rexpr($p) "==" rexpr($c) "==" rexpr($c1) ]
               -> [ (eqT R $p $c)/\(eqT R $c $c1) ]
+*)
+| form_eq_eq [ rexpr($p) "==" rexpr($c) "==" rexpr($c1) ]
+              -> [ (eqT ? $p $c)/\(eqT ? $c $c1) ]
 | form_le_le [ rexpr($p) "<=" rexpr($c) "<=" rexpr($c1) ]
               -> [ (Rle $p $c)/\(Rle $c $c1) ]
 | form_le_lt [ rexpr($p) "<=" rexpr($c) "<" rexpr($c1) ]
@@ -38,7 +43,7 @@ with rformula : constr :=
               -> [ (Rlt $p $c)/\(Rle $c $c1) ]
 | form_lt_lt [ rexpr($p) "<" rexpr($c) "<" rexpr($c1) ]
               -> [ (Rlt $p $c)/\(Rlt $c $c1) ]
-| form_neq  [ rexpr($p) "<>" rexpr($c) ] -> [ ~(eqT R $p $c) ]
+| form_neq  [ rexpr($p) "<>" rexpr($c) ] -> [ ~(eqT ? $p $c) ]
 
 with rexpr : constr :=
   expr_plus [ rexpr($p) "+" rexpr($c) ] -> [ (Rplus $p $c) ]
-- 
cgit v1.2.3