Changement dans le kernel :

   - essai de suppression des dependances debiles. (echec) 
   - Application des patch debian.

Pour ring et field :
   - introduciton de la function de sign et de puissance.
   - Correction de certains bug.
   - supression de ring_replace ....

Pour exact_no_check :
   - ajout de la tactic : vm_cast_no_check (t)
     qui remplace "exact_no_check (t<: type of Goal)"
      (cette version forcais l'evaluation du cast dans le 
       pretypage).




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

1 files changed, 10 insertions, 10 deletions

diff --git a/theories/QArith/Qring.v b/theories/QArith/Qring.v
index 265851ec7..609e82b07 100644
--- a/theories/QArith/Qring.v
+++ b/theories/QArith/Qring.v
@@ -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.