Updated Qpow_tac to work on a a more realistic set of exponent values.

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

1 files changed, 12 insertions, 0 deletions

diff --git a/theories/QArith/Qfield.v b/theories/QArith/Qfield.v
index 3b14a47ce..4d8a80611 100644
--- a/theories/QArith/Qfield.v
+++ b/theories/QArith/Qfield.v
@@ -70,6 +70,8 @@ Ltac Qcst t :=
 
 Ltac Qpow_tac t :=
   match t with
+  | Z0 => N0
+  | Zpos ?n => Ncst (Npos n)
   | Z_of_N ?n => Ncst n
   | NtoZ ?n => Ncst n
   | _ => NotConstant
@@ -112,6 +114,16 @@ Let ex7 : forall x : Q, x-x== 0#1.
   ring.
 Qed.
 
+Let ex8 : forall x : Q, x^1 == x.
+  intro.
+  ring.
+Qed.
+
+Let ex9 : forall x : Q, x^0 == 1.
+  intro.
+  ring.
+Qed.
+
 Example test_field : forall x y : Q, ~(y==0) -> (x/y)*y == x.
 intros.
 field.