diff options
| -rw-r--r-- | contrib/setoid_ring/NArithRing.v | 3 | ||||
| -rw-r--r-- | contrib/setoid_ring/ZArithRing.v | 17 |
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 |