summaryrefslogtreecommitdiff
path: root/theories/ZArith
diff options
context:
space:
mode:
authorGravatar Enrico Tassi <gareuselesinge@debian.org>2016-12-27 16:53:30 +0100
committerGravatar Enrico Tassi <gareuselesinge@debian.org>2016-12-27 16:53:30 +0100
commita4c7f8bd98be2a200489325ff7c5061cf80ab4f3 (patch)
tree26dd9c4aa142597ee09c887ef161d5f0fa5077b6 /theories/ZArith
parent164c6861860e6b52818c031f901ffeff91fca16a (diff)
Imported Upstream version 8.6upstream/8.6
Diffstat (limited to 'theories/ZArith')
-rw-r--r--theories/ZArith/Int.v18
-rw-r--r--theories/ZArith/Zsqrt_compat.v4
-rw-r--r--theories/ZArith/Zwf.v4
3 files changed, 15 insertions, 11 deletions
diff --git a/theories/ZArith/Int.v b/theories/ZArith/Int.v
index d210792f..72021f2e 100644
--- a/theories/ZArith/Int.v
+++ b/theories/ZArith/Int.v
@@ -225,11 +225,11 @@ Module MoreInt (Import I:Int).
(** [int] to [ExprI] *)
Ltac i2ei trm :=
- match constr:trm with
- | 0 => constr:EI0
- | 1 => constr:EI1
- | 2 => constr:EI2
- | 3 => constr:EI3
+ match constr:(trm) with
+ | 0 => constr:(EI0)
+ | 1 => constr:(EI1)
+ | 2 => constr:(EI2)
+ | 3 => constr:(EI3)
| ?x + ?y => let ex := i2ei x with ey := i2ei y in constr:(EIadd ex ey)
| ?x - ?y => let ex := i2ei x with ey := i2ei y in constr:(EIsub ex ey)
| ?x * ?y => let ex := i2ei x with ey := i2ei y in constr:(EImul ex ey)
@@ -241,7 +241,7 @@ Module MoreInt (Import I:Int).
(** [Z] to [ExprZ] *)
with z2ez trm :=
- match constr:trm with
+ match constr:(trm) with
| (?x + ?y)%Z => let ex := z2ez x with ey := z2ez y in constr:(EZadd ex ey)
| (?x - ?y)%Z => let ex := z2ez x with ey := z2ez y in constr:(EZsub ex ey)
| (?x * ?y)%Z => let ex := z2ez x with ey := z2ez y in constr:(EZmul ex ey)
@@ -254,7 +254,7 @@ Module MoreInt (Import I:Int).
(** [Prop] to [ExprP] *)
Ltac p2ep trm :=
- match constr:trm with
+ match constr:(trm) with
| (?x <-> ?y) => let ex := p2ep x with ey := p2ep y in constr:(EPequiv ex ey)
| (?x -> ?y) => let ex := p2ep x with ey := p2ep y in constr:(EPimpl ex ey)
| (?x /\ ?y) => let ex := p2ep x with ey := p2ep y in constr:(EPand ex ey)
@@ -451,4 +451,8 @@ Module Z_as_Int <: Int.
Lemma i2z_ltb n p : ltb n p = Z.ltb (i2z n) (i2z p).
Proof. reflexivity. Qed.
+ (** Compatibility notations for Coq v8.4 *)
+ Notation plus := add (compat "8.4").
+ Notation minus := sub (compat "8.4").
+ Notation mult := mul (compat "8.4").
End Z_as_Int.
diff --git a/theories/ZArith/Zsqrt_compat.v b/theories/ZArith/Zsqrt_compat.v
index b80eb445..f4baba19 100644
--- a/theories/ZArith/Zsqrt_compat.v
+++ b/theories/ZArith/Zsqrt_compat.v
@@ -30,12 +30,12 @@ Local Open Scope Z_scope.
Ltac compute_POS :=
match goal with
| |- context [(Zpos (xI ?X1))] =>
- match constr:X1 with
+ match constr:(X1) with
| context [1%positive] => fail 1
| _ => rewrite (Pos2Z.inj_xI X1)
end
| |- context [(Zpos (xO ?X1))] =>
- match constr:X1 with
+ match constr:(X1) with
| context [1%positive] => fail 1
| _ => rewrite (Pos2Z.inj_xO X1)
end
diff --git a/theories/ZArith/Zwf.v b/theories/ZArith/Zwf.v
index 1ac00bdd..90754af3 100644
--- a/theories/ZArith/Zwf.v
+++ b/theories/ZArith/Zwf.v
@@ -56,7 +56,7 @@ Section wf_proof.
End wf_proof.
-Hint Resolve Zwf_well_founded: datatypes v62.
+Hint Resolve Zwf_well_founded: datatypes.
(** We also define the other family of relations:
@@ -88,4 +88,4 @@ Section wf_proof_up.
End wf_proof_up.
-Hint Resolve Zwf_up_well_founded: datatypes v62.
+Hint Resolve Zwf_up_well_founded: datatypes.