From eca90ac82b764d8be84b31489f21b4c57e6d9140 Mon Sep 17 00:00:00 2001
From: Allan Blanchard <allan.blanchard@cea.fr>
Date: Mon, 2 Dec 2019 15:43:44 +0100
Subject: [PATCH] [WP+Coq] 8.10 compatibility

---
 src/plugins/wp/configure.ac                   |  2 +-
 src/plugins/wp/share/coqwp/Bits.v             |  2 +-
 src/plugins/wp/share/coqwp/BuiltIn.v          |  2 +-
 src/plugins/wp/share/coqwp/Cbits.v            | 12 ++--
 src/plugins/wp/share/coqwp/Qedlib.v           | 54 +++++++--------
 src/plugins/wp/share/coqwp/Vlist.v            |  4 +-
 src/plugins/wp/share/coqwp/Zbits.v            | 68 +++++++++----------
 src/plugins/wp/share/coqwp/int/Abs.v          |  4 +-
 .../wp/share/coqwp/int/ComputerDivision.v     |  8 +--
 .../coqwp/int/ComputerOfEuclideanDivision.v   |  2 +-
 .../wp/share/coqwp/int/EuclideanDivision.v    | 12 ++--
 .../wp/share/coqwp/int/Exponentiation.v       | 12 ++--
 src/plugins/wp/share/coqwp/int/Int.v          |  4 +-
 src/plugins/wp/share/coqwp/int/MinMax.v       | 20 +++---
 src/plugins/wp/share/coqwp/int/Power.v        |  4 +-
 15 files changed, 105 insertions(+), 105 deletions(-)

diff --git a/src/plugins/wp/configure.ac b/src/plugins/wp/configure.ac
index 0185710fc06..6071257d209 100644
--- a/src/plugins/wp/configure.ac
+++ b/src/plugins/wp/configure.ac
@@ -82,7 +82,7 @@ if test "$ENABLE_WP" != "no"; then
     if test "$COQC" = "yes" ; then
       COQVERSION=`coqc -v | sed -n -e 's|.*version* *\([[^ ]]*\) .*$|\1|p' `
       case $COQVERSION in
-        8.7*|8.8*|8.9*|trunk)
+        8.7*|8.8*|8.9*|8.10*|trunk)
           AC_MSG_RESULT(coqc version $COQVERSION found)
           ;;
         *)
diff --git a/src/plugins/wp/share/coqwp/Bits.v b/src/plugins/wp/share/coqwp/Bits.v
index 624a253f499..14ede3c3af1 100644
--- a/src/plugins/wp/share/coqwp/Bits.v
+++ b/src/plugins/wp/share/coqwp/Bits.v
@@ -460,7 +460,7 @@ Proof.
 Qed.					      
 					      
 Remark NxHpos_div2_p: forall n:N,
-  (0 < n)%N -> NxHpos (Ndiv2 n) = pred (NxHpos n).
+  (0 < n)%N -> NxHpos (N.div2 n) = pred (NxHpos n).
 Proof.
   destruct n.
   (** zero *)
diff --git a/src/plugins/wp/share/coqwp/BuiltIn.v b/src/plugins/wp/share/coqwp/BuiltIn.v
index c7b225032cb..097c5eeea2c 100644
--- a/src/plugins/wp/share/coqwp/BuiltIn.v
+++ b/src/plugins/wp/share/coqwp/BuiltIn.v
@@ -26,7 +26,7 @@ Global Instance int_WhyType : WhyType int.
 Proof.
 split.
 exact Z0.
-exact Z_eq_dec.
+exact Z.eq_dec.
 Qed.
 
 Notation real := R.
diff --git a/src/plugins/wp/share/coqwp/Cbits.v b/src/plugins/wp/share/coqwp/Cbits.v
index 2cedd5c8b56..a390807d456 100644
--- a/src/plugins/wp/share/coqwp/Cbits.v
+++ b/src/plugins/wp/share/coqwp/Cbits.v
@@ -1182,7 +1182,7 @@ Lemma is_uint_lxor :
   forall (n:Z) (x:Z) (y:Z), (Cint.is_uint n x) -> (Cint.is_uint n y) ->
   ((Cint.to_uint n (lxor x y)) = (lxor x y)).
 Proof.
-  intro n; is_uint_bitwise xorb (Zabs_nat n). 
+  intro n; is_uint_bitwise xorb (Z.abs_nat n).
 Qed.
 
 (** * Some C-Integer Bits Conversions are identity *)
@@ -1192,7 +1192,7 @@ Lemma is_uint_lor :
   forall (n:Z) (x:Z) (y:Z), (Cint.is_uint n x) -> (Cint.is_uint n y) ->
   ((Cint.to_uint n (lor x y)) = (lor x y)).
 Proof.
-  intro n; is_uint_bitwise orb (Zabs_nat n). 
+  intro n; is_uint_bitwise orb (Z.abs_nat n).
 Qed.
 
 (* Why3 goal *)
@@ -1200,7 +1200,7 @@ Lemma is_uint_land :
   forall (n:Z) (x:Z) (y:Z), (Cint.is_uint n x) -> (Cint.is_uint n y) ->
   ((Cint.to_uint n (land x y)) = (land x y)).
 Proof.
-  intro n; is_uint_bitwise andb (Zabs_nat n). 
+  intro n; is_uint_bitwise andb (Z.abs_nat n).
 Qed.
 
 (* Why3 goal *)
@@ -1486,7 +1486,7 @@ Lemma is_sint_lxor :
   forall (n:Z) (x:Z) (y:Z), (Cint.is_sint n x) -> (Cint.is_sint n y) ->
   ((Cint.to_sint n (lxor x y)) = (lxor x y)).
 Proof.
-  intro n; is_sint_bitwise xorb (Zabs_nat n). 
+  intro n; is_sint_bitwise xorb (Z.abs_nat n).
 Qed.
 
 (* Why3 goal *)
@@ -1494,7 +1494,7 @@ Lemma is_sint_lor :
   forall (n:Z) (x:Z) (y:Z), (Cint.is_sint n x) -> (Cint.is_sint n y) ->
   ((Cint.to_sint n (lor x y)) = (lor x y)).
 Proof.
-  intro n; is_sint_bitwise orb (Zabs_nat n). 
+  intro n; is_sint_bitwise orb (Z.abs_nat n).
 Qed.
 
 (* Why3 goal *)
@@ -1502,7 +1502,7 @@ Lemma is_sint_land :
   forall (n:Z) (x:Z) (y:Z), (Cint.is_sint n x) -> (Cint.is_sint n y) ->
   ((Cint.to_sint n (land x y)) = (land x y)).
 Proof.
-  intro n; is_sint_bitwise andb (Zabs_nat n). 
+  intro n; is_sint_bitwise andb (Z.abs_nat n).
 Qed.
 
 (* Why3 goal *)
diff --git a/src/plugins/wp/share/coqwp/Qedlib.v b/src/plugins/wp/share/coqwp/Qedlib.v
index f251ad04956..2c42f2d4961 100644
--- a/src/plugins/wp/share/coqwp/Qedlib.v
+++ b/src/plugins/wp/share/coqwp/Qedlib.v
@@ -33,12 +33,12 @@ Set Implicit Arguments.
 
 (** ** Tactical *)
 
-Ltac forward := 
-  repeat (first [ split | intros ]) ; 
-  try discriminate ; 
-  try contradiction ; 
-  try tauto ; 
-  try constructor ; 
+Ltac forward :=
+  repeat (first [ split | intros ]) ;
+  try discriminate ;
+  try contradiction ;
+  try tauto ;
+  try constructor ;
   try (apply False_ind ; omega ; fail) ;
   try (apply False_ind ; auto with zarith ; fail) ;
   auto with zarith.
@@ -75,16 +75,16 @@ Inductive reflect (P:Prop) : bool -> Prop :=
   | R_true  : P -> reflect P true
   | R_false : ~P -> reflect P false.
 
-Definition boolean {A : Set} 
-  (f : A -> A -> bool) 
+Definition boolean {A : Set}
+  (f : A -> A -> bool)
   (p : A -> A -> Prop) : Prop := forall x y, reflect (p x y) (f x y).
-  
+
 (*
   forall x y, (f x y = true <-> p x y) /\
               (f x y = false <-> ~(p x y)).
 *)
 
-Ltac case_leq x y := 
+Ltac case_leq x y :=
   generalize (Zle_cases x y) ; induction (Zle_bool x y) ; try omega.
 
 Ltac case_lt x y :=
@@ -130,12 +130,12 @@ Proof.
   unfold boolean. intros x y. by (case_neq x y).
 Qed.
 
-Theorem Zlt_boolean : boolean Zlt_bool Zlt.
+Theorem Zlt_boolean : boolean Zlt_bool Z.lt.
 Proof.
   unfold boolean. intros x y. by (case_lt x y).
 Qed.
 
-Theorem Zle_boolean : boolean Zle_bool Zle.
+Theorem Zle_boolean : boolean Zle_bool Z.le.
 Proof.
   unfold boolean. intros x y. by (case_leq x y).
 Qed.
@@ -156,7 +156,7 @@ Hypothesis Aneq_boolean : forall A : Set, boolean (@Aneq_bool A) (fun x y => x<>
 
 (** ** Integer Induction (after a given rank) *)
 
-Theorem Z_induction(m : Z)(P : Z -> Prop) : 
+Theorem Z_induction(m : Z)(P : Z -> Prop) :
   (forall n, n <= m -> P n ) ->
   (forall n, n >= m -> P n -> P (n+1)) ->
   (forall n, P n).
@@ -165,12 +165,12 @@ Proof.
   induction (Z_le_dec n m) ; auto with zarith.
   apply Z.le_ind with (n := m) ; auto with zarith.
   unfold Morphisms.Proper.
-  unfold Morphisms.respectful. 
+  unfold Morphisms.respectful.
   intros. rewrite H1. intuition.
   intros. apply H0; auto with zarith.
 Qed.
 
-Theorem Z_induction_rank(m : Z)(P : Z -> Prop) : 
+Theorem Z_induction_rank(m : Z)(P : Z -> Prop) :
   P m ->
   (forall n, m <= n -> P n -> P (n+1)) ->
   (forall n, m <= n -> P n).
@@ -180,7 +180,7 @@ Proof.
   + intros.
     apply Z.le_ind with (n := m) ; auto with zarith.
     unfold Morphisms.Proper.
-    unfold Morphisms.respectful. 
+    unfold Morphisms.respectful.
     intros. rewrite H1. intuition.
    + intros. auto with zarith.
 Qed.
@@ -257,7 +257,7 @@ Qed.
 Definition Cdiv (n d : Z) : Z :=
   match n , d with
     | 0 , _ | _ , 0 => 0
-    | Zpos a , Zpos b 
+    | Zpos a , Zpos b
     | Zneg a , Zneg b => (Zpos a/Zpos b)
     | Zpos a , Zneg b
     | Zneg a , Zpos b => (-(Zpos a/Zpos b))
@@ -269,7 +269,7 @@ Definition Cmod (n d : Z) : Z :=
     | Zpos a , Zpos b
     | Zpos a , Zneg b => ( (Zpos a) mod (Zpos b) )
     | Zneg a , Zpos b
-    | Zneg a , Zneg b => (-( (Zpos a) mod (Zpos b) )) 
+    | Zneg a , Zneg b => (-( (Zpos a) mod (Zpos b) ))
   end.
 
 Lemma Cdiv_cases : forall n d,
@@ -279,7 +279,7 @@ Lemma Cdiv_cases : forall n d,
   ((n <= 0) -> (d < 0) -> Cdiv n d = (-n)/(-d)).
 Proof.
   intros.
-  destruct n as [|a|a] ; 
+  destruct n as [|a|a] ;
   destruct d as [|b|b] ;
   intuition ;
   by auto with zarith.
@@ -292,14 +292,14 @@ Lemma Cmod_cases : forall n d,
   ((n <= 0) -> (d < 0) -> Cmod n d = -((-n) mod (-d))).
 Proof.
   intros.
-  destruct n as [|a|a] ; 
+  destruct n as [|a|a] ;
   destruct d as [|b|b] ;
   intuition ;
   by auto with zarith.
 Qed.
 
-Theorem Cdiv_enclidian : 
-  forall (n d : Z), 
+Theorem Cdiv_enclidian :
+  forall (n d : Z),
   d <> 0 ->
   let q := Cdiv n d in let r := Cmod n d in
   (q * d + r = n).
@@ -307,11 +307,11 @@ Proof.
   intros n d NEQ q r.
   assert (OPP: forall p, (- (Zneg p) = Zpos p)) by auto with zarith.
   assert (NEG: forall p, (Zneg p = - (Zpos p))) by auto with zarith.
-  destruct n as [|a|a] ; 
+  destruct n as [|a|a] ;
   destruct d as [|b|b] ; auto with zarith ;
-  unfold Cdiv in q ; unfold Cmod in r ; 
-  unfold q ; unfold r ; 
-  repeat rewrite OPP ; repeat rewrite NEG ; 
+  unfold Cdiv in q ; unfold Cmod in r ;
+  unfold q ; unfold r ;
+  repeat rewrite OPP ; repeat rewrite NEG ;
   rewrite (Zmod_eq_full (Zpos a) (Zpos b)) ; try discriminate ;
   try ring.
 Qed.
@@ -323,7 +323,7 @@ Lemma Cmod_less : forall n d,
   ((n <= 0) -> (d < 0) ->  d <  Cmod n d <= 0).
 Proof.
   intros.
-  destruct n as [|a|a] ; 
+  destruct n as [|a|a] ;
   destruct d as [|b|b] ;
   intuition ; simpl ; forward ;
   generalize (Z_mod_lt (Zpos a) (Zpos b) (Zgt_pos_0 b)) ;
diff --git a/src/plugins/wp/share/coqwp/Vlist.v b/src/plugins/wp/share/coqwp/Vlist.v
index e4f1f454f37..e642bb8fb17 100644
--- a/src/plugins/wp/share/coqwp/Vlist.v
+++ b/src/plugins/wp/share/coqwp/Vlist.v
@@ -76,7 +76,7 @@ Definition repeat {a:Type} {a_WT:WhyType a} : (list a) -> Z -> list a.
   exact(fun w n  => match n with
                    | Z0 => nil
                    | Zneg _ => nil
-                   | other => repeat_nat a w (Zabs_nat (n-1))
+                   | other => repeat_nat a w (Z.abs_nat (n-1))
                    end).
 Defined.
 
@@ -89,7 +89,7 @@ Defined.
 Definition nth {a:Type} {a_WT:WhyType a} : (list a) -> Z -> a.
   exact(fun w n => match n with
                    | Zneg _ => (@why_inhabitant a a_WT)
-                   | other => List.nth (Zabs_nat n) w (@why_inhabitant a a_WT)
+                   | other => List.nth (Z.abs_nat n) w (@why_inhabitant a a_WT)
                    end).
 Defined.
 
diff --git a/src/plugins/wp/share/coqwp/Zbits.v b/src/plugins/wp/share/coqwp/Zbits.v
index 0c02116df5e..8fe2c8c4df0 100644
--- a/src/plugins/wp/share/coqwp/Zbits.v
+++ b/src/plugins/wp/share/coqwp/Zbits.v
@@ -93,37 +93,37 @@ Qed.
 (** Some remarks about absolute value *)
   
 Remark zabs_gt: forall n m: Z, 
-  Zabs m < Zabs n -> (Zabs_nat m < Zabs_nat n)%nat.
+  Z.abs m < Z.abs n -> (Z.abs_nat m < Z.abs_nat n)%nat.
 Proof. 
-  intros. apply (inj_lt_rev (Zabs_nat m) (Zabs_nat n)).
+  intros. apply (inj_lt_rev (Z.abs_nat m) (Z.abs_nat n)).
   rewrite (inj_Zabs_nat n). rewrite (inj_Zabs_nat m). omega.
 Qed.
 					 
 Remark zabs_le: forall n m: Z,
-  Zabs n <= Zabs m -> (Zabs_nat n <= Zabs_nat m)%nat.
+  Z.abs n <= Z.abs m -> (Z.abs_nat n <= Z.abs_nat m)%nat.
 Proof.
-  intros. apply (inj_le_rev (Zabs_nat n) (Zabs_nat m)).
+  intros. apply (inj_le_rev (Z.abs_nat n) (Z.abs_nat m)).
   rewrite (inj_Zabs_nat n). rewrite (inj_Zabs_nat m). omega.
 Qed.
 					 
 Remark zabs_le_plus: forall (n m:Z) (k: nat),
-  Zabs n <= Zabs m -> (Zabs_nat n <= k + Zabs_nat m)%nat.
+  Z.abs n <= Z.abs m -> (Z.abs_nat n <= k + Z.abs_nat m)%nat.
 Proof.
   intros. 
-  apply (inj_le_rev (Zabs_nat n) (k + Zabs_nat m)%nat).
+  apply (inj_le_rev (Z.abs_nat n) (k + Z.abs_nat m)%nat).
   rewrite (inj_Zabs_nat n). rewrite inj_plus. rewrite (inj_Zabs_nat m).
   omega.
 Qed.
 					 
 Remark zabs_nat_zabs: forall n: Z,
-  Zabs_nat (Zabs n) = Zabs_nat n.
+  Z.abs_nat (Z.abs n) = Z.abs_nat n.
 Proof.
   intro.
   rewrite <- (inj_Zabs_nat n). rewrite Zabs_nat_Z_of_nat. auto.
 Qed.
 
 Remark zabs_minus: forall n m: Z,
-  Zabs n <= Zabs m -> (Zabs_nat m - Zabs_nat n)%nat = Zabs_nat (Zabs m - Zabs n).
+  Z.abs n <= Z.abs m -> (Z.abs_nat m - Z.abs_nat n)%nat = Z.abs_nat (Z.abs m - Z.abs n).
 Proof.
   intros. 
   rewrite Zabs_nat_Zminus by (generalize (Zabs_pos n); omega).
@@ -132,7 +132,7 @@ Proof.
 Qed.
 					 
 Remark zabs_plus: forall n m: Z,
-  (Zabs_nat m + Zabs_nat n)%nat = Zabs_nat (Zabs m + Zabs n).
+  (Z.abs_nat m + Z.abs_nat n)%nat = Z.abs_nat (Z.abs m + Z.abs n).
 Proof.
   intros. 
   rewrite Zabs_nat_Zplus.
@@ -1014,7 +1014,7 @@ Proof.
 Qed.
   
 Lemma Z_bitwise_ZxHbound: forall (f: bool -> bool -> bool) (x y: Z),
-   ZxHbound (Z_bitwise f x y) <= Zmax (ZxHbound x) (ZxHbound y).
+   ZxHbound (Z_bitwise f x y) <= Z.max (ZxHbound x) (ZxHbound y).
 Proof.
   intros f x y.
   generalize (Z_bitwise_ZxHpos f x y).
@@ -1043,7 +1043,7 @@ Proof.
   generalize (Z_bitwise_ZxHbound f x y).
   pose (zxy := Z_bitwise f x y); fold zxy.
   generalize (ZxHrange zxy).
-  apply Zmax_case_strong.
+  apply Z.max_case_strong.
   (** ZxHbound y <= ZxHbound x *)
   + intros Ryx Rzxy.
     destruct Rzxy as [ bound_neg bound_pos ].
@@ -1128,7 +1128,7 @@ Proof.
   generalize (Z_bitwise_ZxHbound f x y).
   pose (zxy := Z_bitwise f x y); fold zxy; fold zxy in Bz.
   generalize (ZxHrange zxy).
-  apply Zmax_case_strong.
+  apply Z.max_case_strong.
   (** ZxHbound y <= ZxHbound x *)
   + intros Ryx Rzxy.
     destruct Rzxy as [ Bneg Bpos ].
@@ -1227,7 +1227,7 @@ Qed.
 Parameter lsl_undef: Z -> Z -> Z.
 
 Definition lsl_def (x:Z) (n:Z): Z :=
-  lsl_shift_def x (Zabs_nat n).
+  lsl_shift_def x (Z.abs_nat n).
 
 Definition lsl (x : Z) (y : Z) : Z :=
   if Zle_bool 0 y then lsl_def x y
@@ -1249,7 +1249,7 @@ Qed.
 Parameter lsr_undef: Z -> Z -> Z.
 
 Definition lsr_def (x:Z) (n:Z): Z :=
-  lsr_shift_def x (Zabs_nat n).
+  lsr_shift_def x (Z.abs_nat n).
 
 Definition lsr (x : Z) (y : Z) : Z :=
   if Zle_bool 0 y then lsr_def x y
@@ -1266,15 +1266,15 @@ Qed.
 (** ** Properties of shifting operators *)
 
 Theorem Zbit_lsl: forall (x n: Z) (k: nat), 
-  Zbit (lsl_def x n) k = if (Zle_bool (Zabs n) (Z_of_nat k)) then Zbit x (Zabs_nat ((Z_of_nat k) - (Zabs n))) else false.
+  Zbit (lsl_def x n) k = if (Zle_bool (Z.abs n) (Z_of_nat k)) then Zbit x (Z.abs_nat ((Z_of_nat k) - (Z.abs n))) else false.
 Proof.
   intros. unfold lsl_def. 
   rewrite lsl_arithmetic_shift. unfold lsl_arithmetic_def.
   rewrite Zbit_shift_l.
-  case_leq (Zabs n) (Z_of_nat k).
+  case_leq (Z.abs n) (Z_of_nat k).
   (** case |n| <= k *) 
   + intro LEQ.
-    cut (leb (Zabs_nat n) k= true).
+    cut (leb (Z.abs_nat n) k= true).
     { intro LEB. rewrite LEB. f_equal.
       rewrite Zabs_nat_Zminus; try split; try apply Zabs_pos; auto.
       rewrite Zabs_nat_Z_of_nat.
@@ -1285,7 +1285,7 @@ Proof.
     auto.
   (** case |n| > k *) 
   + intro GT.
-    cut (leb (Zabs_nat n) k = false).
+    cut (leb (Z.abs_nat n) k = false).
     intro GTB. rewrite GTB. auto. 
     apply leb_correct_conv.
     rewrite <- (Zabs_nat_Z_of_nat k).
@@ -1295,7 +1295,7 @@ Proof.
 Qed.
 					 
 Theorem Zbit_lsr: forall (x n: Z) (k: nat),
-  Zbit (lsr_def x n) k = Zbit x (k + (Zabs_nat n))%nat.
+  Zbit (lsr_def x n) k = Zbit x (k + (Z.abs_nat n))%nat.
 Proof.
   intros. 
   (** left  term *) 
@@ -1306,14 +1306,14 @@ Proof.
 Qed.
 
 Lemma lsl_of_lsl: forall (n m: Z) (x:Z),
-  lsl_def (lsl_def x n) m = lsl_def x (Zabs n + Zabs m).
+  lsl_def (lsl_def x n) m = lsl_def x (Z.abs n + Z.abs m).
 Proof.
   intros. unfold lsl_def. 
   rewrite <- zabs_plus.
   rewrite lsl_arithmetic_shift.
   unfold lsl_arithmetic_def. 
-  (replace (x * two_power_nat (Zabs_nat n) * two_power_nat (Zabs_nat m))
-        with (x *(two_power_nat (Zabs_nat n) * two_power_nat (Zabs_nat m))) by ring).
+  (replace (x * two_power_nat (Z.abs_nat n) * two_power_nat (Z.abs_nat m))
+        with (x *(two_power_nat (Z.abs_nat n) * two_power_nat (Z.abs_nat m))) by ring).
   f_equal.
   repeat rewrite two_power_nat_correct.
   rewrite Zpower_nat_is_exp.
@@ -1321,7 +1321,7 @@ Proof.
 Qed.
 
 Lemma lsr_of_lsr: forall (n m: Z) (x:Z),
-  lsr_def (lsr_def x n) m = lsr_def x (Zabs n + Zabs m).
+  lsr_def (lsr_def x n) m = lsr_def x (Z.abs n + Z.abs m).
 Proof.
   intros. unfold lsr_def. 
   rewrite <- zabs_plus.
@@ -1339,7 +1339,7 @@ Qed.
 
 
 Lemma lsr_of_lsl: forall (n m: Z) (x:Z),
-  Zabs n <= Zabs m -> lsr_def (lsl_def x n) m = lsr_def x (Zabs m - Zabs n).
+  Z.abs n <= Z.abs m -> lsr_def (lsl_def x n) m = lsr_def x (Z.abs m - Z.abs n).
 Proof.
   intros. unfold lsr_def. 
   rewrite <- zabs_minus by auto.
@@ -1350,10 +1350,10 @@ Proof.
   unfold lsl_def. unfold lsl_shift_def.
   rewrite Z_decomp_recomp.
   unfold bitwise_lsl. unfold btest at 1.
-  rewrite (leb_correct (Zabs_nat n) (k + Zabs_nat m)).
+  rewrite (leb_correct (Z.abs_nat n) (k + Z.abs_nat m)).
   f_equal.
   (** arg 1 *) 
-  + rewrite (inj_eq_rev (k + Zabs_nat m - Zabs_nat n) (k + (Zabs_nat m - Zabs_nat n))). 
+  + rewrite (inj_eq_rev (k + Z.abs_nat m - Z.abs_nat n) (k + (Z.abs_nat m - Z.abs_nat n))).
     auto.
     rewrite inj_minus1 by (apply zabs_le_plus; omega). 
     repeat rewrite inj_plus. 
@@ -1801,7 +1801,7 @@ Local Ltac lsl_distrib_r lop z :=
   let k := fresh in
   intros; unfold lop; Zbit_bitwise k;
   repeat rewrite Zbit_lsl; rewrite Zbit_bitwise;
-  case_leq (Zabs z) (Z_of_nat k);
+  case_leq (Z.abs z) (Z_of_nat k);
     [ (intro; trivial) | trivial ].
 
 (** Distributive lsl lor *)						       
@@ -2066,7 +2066,7 @@ Proof.
   intros b x y Ry Rx Rb.
   apply Zle_is_le_bool in Ry; unfold lsr; rewrite Ry.
   unfold lsr_def. rewrite lsr_arithmetic_shift. unfold lsr_arithmetic_def.
-  pose (d := two_power_nat (Zabs_nat y)); fold d.
+  pose (d := two_power_nat (Z.abs_nat y)); fold d.
   assert (PWR2: 0 < d) by apply two_power_nat_is_positive.
   apply Zdiv_lt_upper_bound; auto.
   assert (b <= b * d) by apply (upper_positive_mult_positive d b Rb PWR2).
@@ -2079,7 +2079,7 @@ Proof.
   intros b x y Ry Rx Rb.
   apply Zle_is_le_bool in Ry; unfold lsr; rewrite Ry.
   unfold lsr_def. rewrite lsr_arithmetic_shift. unfold lsr_arithmetic_def.
-  pose (d := two_power_nat (Zabs_nat y)); fold d.
+  pose (d := two_power_nat (Z.abs_nat y)); fold d.
   assert (PWR2: 0 < d) by apply two_power_nat_is_positive.
   apply Zdiv_le_lower_bound; auto.
   assert (b * d <= b) by apply (lower_negative_mult_positive d b Rb PWR2).
@@ -2155,7 +2155,7 @@ Parameter zbit_test_undef: Z -> Z -> bool.
 
 (* Extended version for negative value. *)
 Definition zbit_test_def (x:Z) (n:Z): bool :=
-  Zbit x (Zabs_nat n).	
+  Zbit x (Z.abs_nat n).
 					
 Theorem zbit_test_ext: forall x y: Z,
   (forall n, zbit_test_def x n = zbit_test_def y n) -> x=y.
@@ -2203,7 +2203,7 @@ Local Ltac bit_extraction bin_op :=
 (** ** Link between Bit extraction and modulo operator *)
 
 Theorem uint_mod_two_power_extraction: forall (n:nat) (m x:Z),
-  zbit_test_def (x mod (two_power_nat n)) m = if leb n (Zabs_nat m) then false else zbit_test_def x m.
+  zbit_test_def (x mod (two_power_nat n)) m = if leb n (Z.abs_nat m) then false else zbit_test_def x m.
 Proof.
   intros.
   unfold zbit_test_def.
@@ -2214,8 +2214,8 @@ Qed.
 (** ** Link between Bit extraction and bitwise shifting operators *)
 Theorem lsl_extraction: forall x n m: Z, 
   zbit_test_def (lsl_def x n) m =
-    if Zle_bool (Zabs n) (Zabs m) 
-    then zbit_test_def x ((Zabs m) - (Zabs n)) 
+    if Zle_bool (Z.abs n) (Z.abs m)
+    then zbit_test_def x ((Z.abs m) - (Z.abs n))
     else false.
 Proof.
   intros. unfold zbit_test_def.	
@@ -2224,7 +2224,7 @@ Proof.
 Qed.
 					 
 Theorem lsr_extraction: forall x n m: Z, 
-  zbit_test_def (lsr_def x n) m = zbit_test_def x ((Zabs m) + (Zabs n)).
+  zbit_test_def (lsr_def x n) m = zbit_test_def x ((Z.abs m) + (Z.abs n)).
 Proof.
   intros. unfold zbit_test_def. 
   (** right term *) 
diff --git a/src/plugins/wp/share/coqwp/int/Abs.v b/src/plugins/wp/share/coqwp/int/Abs.v
index b6fe3478d67..e82ef0f39e5 100644
--- a/src/plugins/wp/share/coqwp/int/Abs.v
+++ b/src/plugins/wp/share/coqwp/int/Abs.v
@@ -25,12 +25,12 @@ Lemma abs_def :
   (~ (0%Z <= x)%Z -> ((ZArith.BinInt.Z.abs x) = (-x)%Z)).
 intros x.
 split ; intros H.
-now apply Zabs_eq.
+now apply Z.abs_eq.
 apply Zabs_non_eq.
 apply Znot_gt_le.
 contradict H.
 apply Zlt_le_weak.
-now apply Zgt_lt.
+now apply Z.gt_lt.
 Qed.
 
 (* Why3 goal *)
diff --git a/src/plugins/wp/share/coqwp/int/ComputerDivision.v b/src/plugins/wp/share/coqwp/int/ComputerDivision.v
index 060d4cdf041..ba0c9caf114 100644
--- a/src/plugins/wp/share/coqwp/int/ComputerDivision.v
+++ b/src/plugins/wp/share/coqwp/int/ComputerDivision.v
@@ -40,9 +40,9 @@ Lemma Div_bound :
 intros x y (Hx,Hy).
 split.
 now apply Z.quot_pos.
-destruct (Z_eq_dec y 1) as [H|H].
+destruct (Z.eq_dec y 1) as [H|H].
 rewrite H, Z.quot_1_r.
-apply Zle_refl.
+apply Z.le_refl.
 destruct (Zle_lt_or_eq 0 x Hx) as [H'|H'].
 apply Zlt_le_weak.
 apply Z.quot_lt with (1 := H').
@@ -57,10 +57,10 @@ Lemma Mod_bound :
   ((ZArith.BinInt.Z.rem x y) < (ZArith.BinInt.Z.abs y))%Z.
 intros x y Zy.
 destruct (Zle_or_lt 0 x) as [Hx|Hx].
-refine ((fun H => conj (Zlt_le_trans _ 0 _ _ (proj1 H)) (proj2 H)) _).
+refine ((fun H => conj (Z.lt_le_trans _ 0 _ _ (proj1 H)) (proj2 H)) _).
 clear -Zy ; zify ; omega.
 now apply Zrem_lt_pos.
-refine ((fun H => conj (proj1 H) (Zle_lt_trans _ 0 _ (proj2 H) _)) _).
+refine ((fun H => conj (proj1 H) (Z.le_lt_trans _ 0 _ (proj2 H) _)) _).
 clear -Zy ; zify ; omega.
 apply Zrem_lt_neg with (2 := Zy).
 now apply Zlt_le_weak.
diff --git a/src/plugins/wp/share/coqwp/int/ComputerOfEuclideanDivision.v b/src/plugins/wp/share/coqwp/int/ComputerOfEuclideanDivision.v
index fc2edd83eb1..f9fb43d9194 100644
--- a/src/plugins/wp/share/coqwp/int/ComputerOfEuclideanDivision.v
+++ b/src/plugins/wp/share/coqwp/int/ComputerOfEuclideanDivision.v
@@ -19,7 +19,7 @@ Require int.EuclideanDivision.
 Require int.ComputerDivision.
 
 Lemma on_pos_euclidean_is_div:
-  forall n d, (int.EuclideanDivision.div n (Zpos d)) = Zdiv n (Zpos d).
+  forall n d, (int.EuclideanDivision.div n (Zpos d)) = Z.div n (Zpos d).
 intros n d.
 unfold EuclideanDivision.div.
 assert (0 < Z.pos d)%Z by reflexivity.
diff --git a/src/plugins/wp/share/coqwp/int/EuclideanDivision.v b/src/plugins/wp/share/coqwp/int/EuclideanDivision.v
index 9d614fb7776..45c05b8a8ab 100644
--- a/src/plugins/wp/share/coqwp/int/EuclideanDivision.v
+++ b/src/plugins/wp/share/coqwp/int/EuclideanDivision.v
@@ -20,8 +20,8 @@ Require int.Abs.
 Definition div : Z -> Z -> Z.
 intros x y.
 case (Z_le_dec 0 (Zmod x y)) ; intros H.
-exact (Zdiv x y).
-exact (Zdiv x y + 1)%Z.
+exact (Z.div x y).
+exact (Z.div x y + 1)%Z.
 Defined.
 
 (* Why3 goal *)
@@ -87,16 +87,16 @@ unfold div.
 case Z_le_dec ; intros H.
 split.
 apply Z_div_pos with (2 := Hx).
-now apply Zlt_gt.
-destruct (Z_eq_dec y 1) as [H'|H'].
+now apply Z.lt_gt.
+destruct (Z.eq_dec y 1) as [H'|H'].
 rewrite H', Zdiv_1_r.
-apply Zle_refl.
+apply Z.le_refl.
 rewrite <- (Zdiv_1_r x) at 2.
 apply Zdiv_le_compat_l with (1 := Hx).
 omega.
 elim H.
 apply Z_mod_lt.
-now apply Zlt_gt.
+now apply Z.lt_gt.
 Qed.
 
 (* Why3 goal *)
diff --git a/src/plugins/wp/share/coqwp/int/Exponentiation.v b/src/plugins/wp/share/coqwp/int/Exponentiation.v
index 0aa04b60e8e..59490cede59 100644
--- a/src/plugins/wp/share/coqwp/int/Exponentiation.v
+++ b/src/plugins/wp/share/coqwp/int/Exponentiation.v
@@ -42,7 +42,7 @@ Hypothesis Unit_def_r : forall (x:t), ((infix_as x one) = x).
 (* Why3 goal *)
 Definition power : t -> Z -> t.
 intros x n.
-exact (iter_nat (Zabs_nat n) t (fun acc => infix_as x acc) one).
+exact (iter_nat (Z.abs_nat n) t (fun acc => infix_as x acc) one).
 Defined.
 
 (* Why3 goal *)
@@ -58,7 +58,7 @@ Lemma Power_s :
 Proof.
 intros x n h1.
 unfold power.
-fold (Zsucc n).
+fold (Z.succ n).
 now rewrite Zabs_nat_Zsucc.
 Qed.
 
@@ -88,7 +88,7 @@ revert n Hn.
 apply natlike_ind.
 apply sym_eq, Unit_def_l.
 intros n Hn IHn.
-replace (Zsucc n + m)%Z with ((n + m) + 1)%Z by ring.
+replace (Z.succ n + m)%Z with ((n + m) + 1)%Z by ring.
 rewrite Power_s by auto with zarith.
 rewrite IHn.
 now rewrite <- Assoc, <- Power_s.
@@ -104,7 +104,7 @@ revert m Hm.
 apply natlike_ind.
 now rewrite Zmult_0_r, 2!Power_0.
 intros m Hm IHm.
-replace (n * Zsucc m)%Z with (n + n * m)%Z by ring.
+replace (n * Z.succ m)%Z with (n + n * m)%Z by ring.
 rewrite Power_sum by auto with zarith.
 rewrite IHm.
 now rewrite <- Power_s.
@@ -119,7 +119,7 @@ intros x y comm.
 apply natlike_ind.
 now rewrite Power_0, Unit_def_r, Unit_def_l.
 intros n Hn IHn.
-unfold Zsucc.
+unfold Z.succ.
 rewrite (Power_s _ _ Hn).
 rewrite Assoc.
 rewrite IHn.
@@ -139,7 +139,7 @@ apply natlike_ind.
 rewrite 3!Power_0.
 now rewrite Unit_def_r.
 intros n Hn IHn.
-unfold Zsucc.
+unfold Z.succ.
 rewrite 3!(Power_s _ _ Hn).
 rewrite IHn.
 rewrite <- Assoc.
diff --git a/src/plugins/wp/share/coqwp/int/Int.v b/src/plugins/wp/share/coqwp/int/Int.v
index 8447e44455a..09419cb7809 100644
--- a/src/plugins/wp/share/coqwp/int/Int.v
+++ b/src/plugins/wp/share/coqwp/int/Int.v
@@ -123,14 +123,14 @@ Qed.
 Lemma Refl : forall (x:Z), (x <= x)%Z.
 Proof.
 intros x.
-apply Zle_refl.
+apply Z.le_refl.
 Qed.
 
 (* Why3 goal *)
 Lemma Trans :
   forall (x:Z) (y:Z) (z:Z), (x <= y)%Z -> (y <= z)%Z -> (x <= z)%Z.
 Proof.
-exact Zle_trans.
+exact Z.le_trans.
 Qed.
 
 (* Why3 goal *)
diff --git a/src/plugins/wp/share/coqwp/int/MinMax.v b/src/plugins/wp/share/coqwp/int/MinMax.v
index 8510be57857..61d4850c8d6 100644
--- a/src/plugins/wp/share/coqwp/int/MinMax.v
+++ b/src/plugins/wp/share/coqwp/int/MinMax.v
@@ -26,8 +26,8 @@ Lemma min_def :
 Proof.
 intros x y.
 split ; intros H.
-now apply Zmin_l.
-apply Zmin_r.
+now apply Z.min_l.
+apply Z.min_r.
 omega.
 Qed.
 
@@ -42,33 +42,33 @@ Lemma max_def :
 Proof.
 intros x y.
 split ; intros H.
-now apply Zmax_r.
-apply Zmax_l.
+now apply Z.max_r.
+apply Z.max_l.
 omega.
 Qed.
 
 (* Why3 goal *)
 Lemma Min_r :
   forall (x:Z) (y:Z), (y <= x)%Z -> ((ZArith.BinInt.Z.min x y) = y).
-exact Zmin_r.
+exact Z.min_r.
 Qed.
 
 (* Why3 goal *)
 Lemma Max_l :
   forall (x:Z) (y:Z), (y <= x)%Z -> ((ZArith.BinInt.Z.max x y) = x).
-exact Zmax_l.
+exact Z.max_l.
 Qed.
 
 (* Why3 goal *)
 Lemma Min_comm :
   forall (x:Z) (y:Z), ((ZArith.BinInt.Z.min x y) = (ZArith.BinInt.Z.min y x)).
-exact Zmin_comm.
+exact Z.min_comm.
 Qed.
 
 (* Why3 goal *)
 Lemma Max_comm :
   forall (x:Z) (y:Z), ((ZArith.BinInt.Z.max x y) = (ZArith.BinInt.Z.max y x)).
-exact Zmax_comm.
+exact Z.max_comm.
 Qed.
 
 (* Why3 goal *)
@@ -78,7 +78,7 @@ Lemma Min_assoc :
    (ZArith.BinInt.Z.min x (ZArith.BinInt.Z.min y z))).
 Proof.
 intros x y z.
-apply eq_sym, Zmin_assoc.
+apply eq_sym, Z.min_assoc.
 Qed.
 
 (* Why3 goal *)
@@ -88,6 +88,6 @@ Lemma Max_assoc :
    (ZArith.BinInt.Z.max x (ZArith.BinInt.Z.max y z))).
 Proof.
 intros x y z.
-apply eq_sym, Zmax_assoc.
+apply eq_sym, Z.max_assoc.
 Qed.
 
diff --git a/src/plugins/wp/share/coqwp/int/Power.v b/src/plugins/wp/share/coqwp/int/Power.v
index 47be81da9aa..5a4a39baae1 100644
--- a/src/plugins/wp/share/coqwp/int/Power.v
+++ b/src/plugins/wp/share/coqwp/int/Power.v
@@ -46,7 +46,7 @@ intros x n h1.
 rewrite Zpower_exp.
 change (power x 1) with (x * 1)%Z.
 ring.
-now apply Zle_ge.
+now apply Z.le_ge.
 easy.
 Qed.
 
@@ -72,7 +72,7 @@ Lemma Power_sum :
   ((power x (n + m)%Z) = ((power x n) * (power x m))%Z).
 Proof.
 intros x n m Hn Hm.
-now apply Zpower_exp; apply Zle_ge.
+now apply Zpower_exp; apply Z.le_ge.
 Qed.
 
 (* Why3 goal *)
-- 
GitLab