Imported Upstream version 8.1+dfsgupstream/8.1+dfsg

1 files changed, 11 insertions, 11 deletions

diff --git a/theories/QArith/Qring.v b/theories/QArith/Qring.v
index 9d294805..f9aa3e50 100644
--- a/theories/QArith/Qring.v
+++ b/theories/QArith/Qring.v
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: Qring.v 9245 2006-10-17 12:53:34Z notin $ i*)
+(*i $Id: Qring.v 9551 2007-01-29 15:13:35Z bgregoir $ i*)
 
 Require Export Ring.
 Require Export QArith_base.
@@ -37,15 +37,15 @@ Proof.
 Qed.
 
 Ltac isQcst t :=
-  let t := eval hnf in t in
-    match t with
-      Qmake ?n ?d =>
-      match isZcst n with
-        true => isZcst d
-	| _ => false
-      end
-      | _ => false
-    end.
+  match t with
+  | inject_Z ?z => isZcst z
+  | Qmake ?n ?d =>
+    match isZcst n with
+      true => isPcst d
+    | _ => false
+    end
+  | _ => false
+  end.
 
 Ltac Qcst t :=
   match isQcst t with
@@ -74,7 +74,7 @@ Let ex3 : forall x y z : Q, (x+y)+z == x+(y+z).
 Qed.
 
 Let ex4 : (inject_Z 1)+(inject_Z 1)==(inject_Z 2).
-  ring.
+ ring.
 Qed.
 
 Let ex5 : 1+1 == 2#1.