Imported Upstream version 8.6upstream/8.6

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.