Revert "syntax for exponents"

This reverts pottier's commit r13849. It references a
ncring_plugin.cma for which there is no rule. I guess he forgot to
commit something...

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

7 files changed, 5 insertions, 24 deletions

diff --git a/plugins/pluginsbyte.itarget b/plugins/pluginsbyte.itarget
index 402d22d1b..04cbdccb0 100644
--- a/plugins/pluginsbyte.itarget
+++ b/plugins/pluginsbyte.itarget
@@ -13,7 +13,6 @@ 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 c7c855336..bbadfe696 100644
--- a/plugins/pluginsdyn.itarget
+++ b/plugins/pluginsdyn.itarget
@@ -13,7 +13,6 @@ 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 84ba2c6d7..74b3f5275 100644
--- a/plugins/pluginsopt.itarget
+++ b/plugins/pluginsopt.itarget
@@ -13,7 +13,6 @@ 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 421178f40..db56534c9 100644
--- a/plugins/pluginsvo.itarget
+++ b/plugins/pluginsvo.itarget
@@ -2,7 +2,6 @@ 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 46064385a..5ba016074 100644
--- a/plugins/setoid_ring/Cring.v
+++ b/plugins/setoid_ring/Cring.v
@@ -11,7 +11,6 @@
 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.
@@ -57,13 +56,8 @@ 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 (ZN y)}.
+  {power x y := @Ring_theory.pow_N _ cring1 cring_mult x 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 8df45b56e..c83dd4e8d 100644
--- a/plugins/setoid_ring/Cring_tac.v
+++ b/plugins/setoid_ring/Cring_tac.v
@@ -14,7 +14,6 @@ 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.
@@ -213,18 +212,14 @@ 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 == (u + t + z + y + x) ^13.
+Goal forall x y z  t u :R, (x + y + z + t + u)^13%N == (u + t + z + y + x) ^13%N.
 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 == (u + t + z + y + x) ^16.
+Goal forall x y z  t u :R, (x + y + z + t + u)^16%N == (u + t + z + y + x) ^16%N.
 Time cring.(*Finished transaction in 1. secs (0.968852u,0.001s)*)
 Qed.
 *)
@@ -242,10 +237,6 @@ 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.
@@ -255,7 +246,7 @@ Goal forall x y z:R, x * y * z == x * (y * z).
 cring.
 Qed.
 
-Goal forall x y z:R, 3 * x * (2%Z * y * z) == 6 * (x * y) * z.
+Goal forall x y z:R, 3%Z * x * (2%Z * y * z) == 6%Z * (x * y) * z.
 cring.
 Qed.
 
diff --git a/plugins/setoid_ring/vo.itarget b/plugins/setoid_ring/vo.itarget
index c4a21fd6a..cccd21855 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
+Ring2_tac.vo
\ No newline at end of file