syntax for exponents

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

7 files changed, 24 insertions, 5 deletions

diff --git a/plugins/pluginsbyte.itarget b/plugins/pluginsbyte.itarget
index 04cbdccb01..402d22d1be 100644
--- a/plugins/pluginsbyte.itarget
+++ b/plugins/pluginsbyte.itarget
@@ -13,6 +13,7 @@ xml/xml_plugin.cma
 subtac/subtac_plugin.cma
 ring/ring_plugin.cma
 cc/cc_plugin.cma
+ncring/ncring_plugin.cma
 nsatz/nsatz_plugin.cma
 funind/recdef_plugin.cma
 syntax/ascii_syntax_plugin.cma
diff --git a/plugins/pluginsdyn.itarget b/plugins/pluginsdyn.itarget
index bbadfe696e..c7c8553362 100644
--- a/plugins/pluginsdyn.itarget
+++ b/plugins/pluginsdyn.itarget
@@ -13,6 +13,7 @@ xml/xml_plugin.cmxs
 subtac/subtac_plugin.cmxs
 ring/ring_plugin.cmxs
 cc/cc_plugin.cmxs
+ncring/ncring_plugin.cmxs
 nsatz/nsatz_plugin.cmxs
 funind/recdef_plugin.cmxs
 syntax/ascii_syntax_plugin.cmxs
diff --git a/plugins/pluginsopt.itarget b/plugins/pluginsopt.itarget
index 74b3f5275f..84ba2c6d74 100644
--- a/plugins/pluginsopt.itarget
+++ b/plugins/pluginsopt.itarget
@@ -13,6 +13,7 @@ xml/xml_plugin.cmxa
 subtac/subtac_plugin.cmxa
 ring/ring_plugin.cmxa
 cc/cc_plugin.cmxa
+ncring/ncring_plugin.cmxa
 nsatz/nsatz_plugin.cmxa
 funind/recdef_plugin.cmxa
 syntax/ascii_syntax_plugin.cmxa
diff --git a/plugins/pluginsvo.itarget b/plugins/pluginsvo.itarget
index db56534c98..421178f404 100644
--- a/plugins/pluginsvo.itarget
+++ b/plugins/pluginsvo.itarget
@@ -2,6 +2,7 @@ dp/vo.otarget
 field/vo.otarget
 fourier/vo.otarget
 funind/vo.otarget
+ncring/vo.otarget
 nsatz/vo.otarget
 micromega/vo.otarget
 omega/vo.otarget
diff --git a/plugins/setoid_ring/Cring.v b/plugins/setoid_ring/Cring.v
index 5ba0160747..46064385a9 100644
--- a/plugins/setoid_ring/Cring.v
+++ b/plugins/setoid_ring/Cring.v
@@ -11,6 +11,7 @@
 Require Import Setoid.
 Require Import BinPos.
 Require Import BinNat.
+Require Export ZArith.
 Require Export Morphisms Setoid Bool.
 Require Import Algebra_syntax.
 Require Import Ring_theory.
@@ -56,8 +57,13 @@ Instance opposite_cring`{R:Type}`{Rr:Cring R} : Opposite R :=
   {opposite x := cring_opp x}.
 Instance equality_cring `{R:Type}`{Rr:Cring R} : Equality :=
   {equality x y := cring_eq x y}.
+Definition ZN(x:Z):=
+  match x with
+    Z0 => N0
+    |Zpos p | Zneg p => Npos p
+end.
 Instance power_cring {R:Type}{Rr:Cring R} : Power:=
-  {power x y := @Ring_theory.pow_N _ cring1 cring_mult x y}.
+  {power x y := @Ring_theory.pow_N _ cring1 cring_mult x (ZN y)}.
 
 Existing Instance cring_setoid.
 Existing Instance cring_plus_comp.
diff --git a/plugins/setoid_ring/Cring_tac.v b/plugins/setoid_ring/Cring_tac.v
index c83dd4e8de..8df45b56e7 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.
 
diff --git a/plugins/setoid_ring/vo.itarget b/plugins/setoid_ring/vo.itarget
index cccd21855d..c4a21fd6aa 100644
--- a/plugins/setoid_ring/vo.itarget
+++ b/plugins/setoid_ring/vo.itarget
@@ -20,4 +20,4 @@ Cring_tac.vo
 Ring2.vo
 Ring2_polynom.vo
 Ring2_initial.vo
-Ring2_tac.vo
\ No newline at end of file
+Ring2_tac.vo