diff options
| -rw-r--r-- | theories/Reals/Exp_prop.v | 2 | ||||
| -rw-r--r-- | 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 a180c4a5b..5c06af34a 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 4733ad3cb..a008cd06e 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) ] |