syntax for exponents

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13897 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 12 insertions, 3 deletions

diff --git a/plugins/setoid_ring/Cring_tac.v b/plugins/setoid_ring/Cring_tac.v
index c83dd4e8d..8df45b56e 100644
--- a/plugins/setoid_ring/Cring_tac.v
+++ b/plugins/setoid_ring/Cring_tac.v
@@ -14,6 +14,7 @@ Require Import Znumtheory.
 Require Import Zdiv_def.
 Require Export Morphisms Setoid Bool.
 Require Import ZArith.
+Open Scope Z_scope.
 Require Import Algebra_syntax.
 Require Import Ring_polynom.
 Require Export Cring.
@@ -212,14 +213,18 @@ Variable R: Type.
 Variable Rr: Cring R.
 Existing Instance Rr.
 
+Goal forall x y z:R, 3%Z * x * (2%Z * y * z) == 6%Z * (x * y) * z.
+cring.
+Qed.
+
 (* reification: 0,7s
 sinon, le reste de la tactique donne le même temps que ring 
 *)
-Goal forall x y z  t u :R, (x + y + z + t + u)^13%N == (u + t + z + y + x) ^13%N.
+Goal forall x y z  t u :R, (x + y + z + t + u)^13 == (u + t + z + y + x) ^13.
 Time cring. (*Finished transaction in 0. secs (0.410938u,0.s)*)
 Qed.
 (*
-Goal forall x y z  t u :R, (x + y + z + t + u)^16%N == (u + t + z + y + x) ^16%N.
+Goal forall x y z  t u :R, (x + y + z + t + u)^16 == (u + t + z + y + x) ^16.
 Time cring.(*Finished transaction in 1. secs (0.968852u,0.001s)*)
 Qed.
 *)
@@ -237,6 +242,10 @@ Time ring.(*Finished transaction in 1. secs (0.914861u,0.s)*)
 Qed.
 *)
 
+Goal forall x y z:R, 6*x^2 + y  == y + 3*2*x^2 + 0 .
+cring.
+Qed.
+
 (*
 Goal forall x y z:R, x + y  == y + x + 0 .
 cring.
@@ -246,7 +255,7 @@ Goal forall x y z:R, x * y * z == x * (y * z).
 cring.
 Qed.
 
-Goal forall x y z:R, 3%Z * x * (2%Z * y * z) == 6%Z * (x * y) * z.
+Goal forall x y z:R, 3 * x * (2%Z * y * z) == 6 * (x * y) * z.
 cring.
 Qed.