From a384c7e9484bb81f07fd27bade2f6a393a076ddf Mon Sep 17 00:00:00 2001
From: roconnor
Date: Mon, 25 Jun 2007 14:04:12 +0000
Subject: 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
---
 theories/QArith/Qfield.v | 12 ++++++++++++
 1 file changed, 12 insertions(+)

diff --git a/theories/QArith/Qfield.v b/theories/QArith/Qfield.v
index 3b14a47ce2..4d8a806115 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.
-- 
cgit v1.2.3