suite de r9362: reconnaissance de qqs injections entre nat, N et Z

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

2 files changed, 17 insertions, 3 deletions

diff --git a/contrib/setoid_ring/NArithRing.v b/contrib/setoid_ring/NArithRing.v
index 65749cb7e8..5c4706651e 100644
--- a/contrib/setoid_ring/NArithRing.v
+++ b/contrib/setoid_ring/NArithRing.v
@@ -19,6 +19,9 @@ Ltac isNcst t :=
   | xI ?p => isNcst p
   | xO ?p => isNcst p
   | xH => constr:true
+  (* nat -> positive *)
+  | P_of_succ_nat ?n => isZcst n
+  (* *)
   | _ => constr:false
   end.
 Ltac Ncst t :=
diff --git a/contrib/setoid_ring/ZArithRing.v b/contrib/setoid_ring/ZArithRing.v
index d2e29cc5c5..84b823d563 100644
--- a/contrib/setoid_ring/ZArithRing.v
+++ b/contrib/setoid_ring/ZArithRing.v
@@ -14,13 +14,24 @@ Set Implicit Arguments.
 
 Ltac isZcst t :=
   match t with
-    Z0 => constr:true
+    Z0 => true
   | Zpos ?p => isZcst p
   | Zneg ?p => isZcst p
   | xI ?p => isZcst p
   | xO ?p => isZcst p
-  | xH => constr:true
-  | _ => constr:false
+  | xH => true
+  (* injection nat -> Z *)
+  | Z_of_nat ?n => isZcst n
+  | O => true
+  | S ?n => isZcst n
+  (* injection N -> Z *)
+  | Z_of_N ?n => isZcst n
+  | N0 => true
+  | Npos ?p => isZcst p
+  (* nat -> positive *)
+  | P_of_succ_nat ?n => isZcst n
+  (* *)
+  | _ => false
   end.
 Ltac Zcst t :=
   match isZcst t with