diff -Nru why3-1.2.1/debian/changelog why3-1.2.1/debian/changelog
--- why3-1.2.1/debian/changelog	2020-02-10 12:57:51.000000000 +0000
+++ why3-1.2.1/debian/changelog	2020-03-08 19:36:59.000000000 +0000
@@ -1,3 +1,32 @@
+why3 (1.2.1-6) unstable; urgency=medium
+
+  * Add build-dependency libnum-ocaml-dev (used to be pulled in by coq)
+  * Bump build-dependency on ocaml, as indicated by opam file
+
+ -- Ralf Treinen <treinen@debian.org>  Sun, 08 Mar 2020 20:36:59 +0100
+
+why3 (1.2.1-5) unstable; urgency=medium
+
+  * debian/rules: include coqvars.mk, and set F:CoqABI substvar, only where
+    that file exists.
+
+ -- Ralf Treinen <treinen@debian.org>  Sun, 08 Mar 2020 17:34:13 +0100
+
+why3 (1.2.1-4) unstable; urgency=medium
+
+  * Support new coq versions:
+    - add patch coq-8.10+11:
+    - invoke autoconf in debian/rules, add it to build-depends
+  * Since coq does no longer build on all release architectures:
+    - Mark the test why3+coq as skip-not-installable
+    - Restrict build-dependencies on coq to amd64 arm64 ppc64 ppc64el sh4
+    - Restrict recommendation of why3-coq to amd64 arm64 ppc64 ppc64el sh4
+    - Build why3-coq only on amd64 arm64 ppc64 ppc64el sh4
+  * Standards-Version 4.5.0 (no change)
+  * Drop override of dh_dwz which is no longer needed.
+
+ -- Ralf Treinen <treinen@debian.org>  Sun, 08 Mar 2020 16:35:43 +0100
+
 why3 (1.2.1-3) unstable; urgency=medium
 
   [ Stéphane Glondu ]
diff -Nru why3-1.2.1/debian/control why3-1.2.1/debian/control
--- why3-1.2.1/debian/control	2020-02-10 12:57:51.000000000 +0000
+++ why3-1.2.1/debian/control	2020-03-08 19:36:59.000000000 +0000
@@ -5,15 +5,18 @@
 Uploaders: Ralf Treinen <treinen@debian.org>
 Build-Depends:
   debhelper-compat (= 12), dh-ocaml,
-  ocaml-nox (>= 3.11.2),
+  autoconf,
+  ocaml-nox (>= 4.05.5),
   ocaml-findlib,
   menhir (>= 20200123),
   libmenhir-ocaml-dev (>= 20200123),
   libzarith-ocaml-dev,
   libsqlite3-ocaml-dev,
   libzip-ocaml-dev,
+  libnum-ocaml-dev,
   libocamlgraph-ocaml-dev,
-  coq, libcoq-ocaml-dev,
+  coq [amd64 arm64 ppc64 ppc64el sh4],
+  libcoq-ocaml-dev [amd64 arm64 ppc64 ppc64el sh4],
   liblablgtk3-ocaml-dev, liblablgtksourceview3-ocaml-dev,
   tex-common
 Build-Depends-Indep:
@@ -22,7 +25,7 @@
   texlive-latex-recommended, texlive-latex-extra,
   texlive-fonts-recommended,
   texlive-bibtex-extra
-Standards-Version: 4.4.1
+Standards-Version: 4.5.0
 Homepage: http://why3.lri.fr/
 Vcs-Git: https://salsa.debian.org/ocaml-team/why3.git
 Vcs-Browser: https://salsa.debian.org/ocaml-team/why3
@@ -33,7 +36,7 @@
   ${shlibs:Depends},
   ${ocaml:Depends},
   ${misc:Depends},
-Recommends: cvc4 | why3-coq | spass | z3 (<< 4.8.7) | alt-ergo (>= 2.0.0)
+Recommends: cvc4 | why3-coq [amd64 arm64 ppc64 ppc64el sh4]| spass | z3 (<< 4.8.7) | alt-ergo (>= 2.0.0)
 Suggests: why3-examples
 Description: Software verification platform
  Why3 is a platform for deductive program verification. It provides a
@@ -57,7 +60,7 @@
  a new external prover if wanted.
 
 Package: why3-coq
-Architecture: any
+Architecture: amd64 arm64 ppc64 ppc64el sh4
 Depends: coq-${F:CoqABI}, ${misc:Depends}, ${ocaml:Depends}, ${shlibs:Depends}
 Recommends: why3
 Description: Coq support for the why3 verification platform
diff -Nru why3-1.2.1/debian/patches/coq-8.10+11 why3-1.2.1/debian/patches/coq-8.10+11
--- why3-1.2.1/debian/patches/coq-8.10+11	1970-01-01 00:00:00.000000000 +0000
+++ why3-1.2.1/debian/patches/coq-8.10+11	2020-03-08 19:36:59.000000000 +0000
@@ -0,0 +1,798 @@
+Description: Support coq versions 8.10.? and 8.11.0
+Authors: Kate Deplaix <kit.ty.kate@disroot.org>,
+  Guillaume Melquiond <guillaume.melquiond@inria.fr>
+Upstream-commits: 38fcc213222ba1cd2493a2126ac7334b6f789b3c,
+  4d48c21d7b9fb8ff7f4a66c996285d9869d8a82e
+
+Index: why3/share/provers-detection-data.conf
+===================================================================
+--- why3.orig/share/provers-detection-data.conf	2020-03-08 08:42:18.093485748 +0100
++++ why3/share/provers-detection-data.conf	2020-03-08 08:42:18.089485725 +0100
+@@ -608,6 +608,8 @@
+ exec = "coqtop"
+ version_switch = "-v"
+ version_regexp = "The Coq Proof Assistant, version \\([^ \n]+\\)"
++version_ok = "^8\.11\.0$"
++version_ok = "^8\.10\.[0-2]$"
+ version_ok = "^8\.9\.[0-1]$"
+ version_ok = "^8\.8\.[0-2]$"
+ version_ok = "^8\.7\.[0-2]$"
+Index: why3/configure.in
+===================================================================
+--- why3.orig/configure.in	2020-03-08 08:42:18.093485748 +0100
++++ why3/configure.in	2020-03-08 08:42:18.089485725 +0100
+@@ -721,6 +721,12 @@
+       8.9*)
+          coq_compat_version="COQ89"
+          ;;
++      8.10*)
++         coq_compat_version="COQ810"
++         ;;
++      8.11*)
++         coq_compat_version="COQ811"
++         ;;
+       *)
+          enable_coq_support=no
+          AC_MSG_WARN(You need Coq 8.5 or later; Coq discarded)
+Index: why3/lib/coq/BuiltIn.v
+===================================================================
+--- why3.orig/lib/coq/BuiltIn.v	2020-03-08 08:42:18.093485748 +0100
++++ why3/lib/coq/BuiltIn.v	2020-03-08 08:42:18.089485725 +0100
+@@ -26,7 +26,7 @@
+ Proof.
+ split.
+ exact Z0.
+-exact Z_eq_dec.
++exact Z.eq_dec.
+ Qed.
+ 
+ Notation real := R.
+Index: why3/lib/coq/bv/BV_Gen.v
+===================================================================
+--- why3.orig/lib/coq/bv/BV_Gen.v	2020-03-08 08:42:18.093485748 +0100
++++ why3/lib/coq/bv/BV_Gen.v	2020-03-08 08:42:18.093485748 +0100
+@@ -51,7 +51,7 @@
+ Fixpoint nth_aux {l} (v : Vector.t bool l) (m : Z) : bool :=
+   match v with
+     | Vector.nil _ => false
+-    | Vector.cons _ b _ tl => if Z_eq_dec m 0 then b else nth_aux tl (Z.pred m)
++    | Vector.cons _ b _ tl => if Z.eq_dec m 0 then b else nth_aux tl (Z.pred m)
+   end.
+ 
+ (* nth helper lemmas *)
+@@ -716,7 +716,7 @@
+   unfold twos_complement.
+   rewrite H.
+   apply Z.lt_sub_0.
+-  apply Zlt_le_trans with (m := Pow2int.pow2 (Z.of_nat (S n))).
++  apply Z.lt_le_trans with (m := Pow2int.pow2 (Z.of_nat (S n))).
+   rewrite Z2Nat.inj_lt.
+   rewrite Nat2Z.id.
+   apply bvec_to_nat_range.
+@@ -752,7 +752,7 @@
+         + rewrite <- H. generalize (bvec_to_nat_range v). intros.
+           eapply Z.lt_sub_0. rewrite <- Z2Nat.id.
+           apply inj_lt. assumption.
+-          eapply Zle_trans. apply (max_int_nat (S m)).
++          eapply Z.le_trans. apply (max_int_nat (S m)).
+           omega.
+       }
+       omega.
+@@ -766,7 +766,7 @@
+         + rewrite H. generalize (bvec_to_nat_range v'). intros.
+           eapply Z.lt_sub_0. rewrite <- Z2Nat.id.
+           apply inj_lt. assumption.
+-          eapply Zle_trans. apply (max_int_nat (S m)).
++          eapply Z.le_trans. apply (max_int_nat (S m)).
+           omega.
+       }
+       omega.
+@@ -969,7 +969,7 @@
+   intros x y H.
+   rewrite mod1_is_mod, mod1_is_mod by trivial.
+   rewrite Z.mod_eq, Z.mod_eq by omega.
+-  intro; cut (Zsucc x / y = x / y).
++  intro; cut (Z.succ x / y = x / y).
+   intro e; rewrite e; omega.
+   rewrite Z.div_unique_pos with (a := Z.succ x) (b := y) (r := (x mod y) + 1) (q := x / y).
+   trivial.
+@@ -1297,10 +1297,9 @@
+ Lemma to_uint_lsl_aux : forall (v:t) (n:nat), ((to_uint (lsl v
+   (Z.of_nat n))) = (mod1 ((to_uint v) * (Pow2int.pow2 (Z.of_nat n)))%Z
+   two_power_size)).
++Proof.
+   intros v n.
+-  rewrite mod1_is_mod.
+-  Focus 2.
+-  easy.
++  rewrite mod1_is_mod by easy.
+   induction n.
+   simpl.
+   apply Zmod_unique with (q := 0).
+@@ -1450,7 +1449,7 @@
+   omega. unfold size_nat in *.
+   apply Z2Nat.inj_le in H1; try omega.
+   rewrite Nat2Z.id in H1; try omega.
+-  eapply Zle_trans. apply (max_int_nat (S last_bit)). omega.
++  eapply Z.le_trans. apply (max_int_nat (S last_bit)). omega.
+ 
+   intuition.
+   unfold zeros, zeros_aux.
+@@ -1948,9 +1947,7 @@
+   rewrite mask_succ_2; simpl.
+   unfold bw_or, nth.
+   rewrite <-nth_aux_map2.
+-  Focus 2.
+-  split; auto with zarith.
+-  apply to_uint_bounds.
++  2: split; auto with zarith; apply to_uint_bounds.
+ 
+   apply orb_true_iff.
+   case (Z_lt_le_dec (to_uint i) 1); intro.
+@@ -2102,10 +2099,6 @@
+   unfold eq_sub, eq_sub_bv.
+   transitivity (eq_aux (bw_and b (lsl_bv (sub (lsl_bv (of_int 1) n) (of_int 1)) i))
+                        (bw_and a (lsl_bv (sub (lsl_bv (of_int 1) n) (of_int 1)) i))); unfold eq_aux.
+-  Focus 2.
+-  split.
+-  apply Extensionality_aux.
+-  intro e; rewrite e; reflexivity.
+   split; intros.
+ 
+   fold nth; rewrite Nth_bw_and, Nth_bw_and by auto.
+@@ -2132,6 +2125,10 @@
+   auto.
+ 
+   unfold nth, nth; rewrite nth_high, nth_high by auto with zarith; reflexivity.
++
++  split.
++  apply Extensionality_aux.
++  intro e; rewrite e; reflexivity.
+ Qed.
+ 
+ (* Why3 goal *)
+Index: why3/lib/coq/bv/Pow2int.v
+===================================================================
+--- why3.orig/lib/coq/bv/Pow2int.v	2020-03-08 08:42:18.093485748 +0100
++++ why3/lib/coq/bv/Pow2int.v	2020-03-08 08:42:18.093485748 +0100
+@@ -49,7 +49,7 @@
+ Lemma pow2pos : forall (i:Z), (0%Z <= i)%Z -> (0%Z < (pow2 i))%Z.
+   intros i h1.
+   Require Import Zorder.
+-  apply Zgt_lt.
++  apply Z.gt_lt.
+   auto using two_p_gt_ZERO.
+ Qed.
+ 
+Index: why3/lib/coq/floating_point/GenFloat.v
+===================================================================
+--- why3.orig/lib/coq/floating_point/GenFloat.v	2020-03-08 08:42:18.093485748 +0100
++++ why3/lib/coq/floating_point/GenFloat.v	2020-03-08 08:42:18.093485748 +0100
+@@ -223,15 +223,15 @@
+ rewrite (mag_unique _ _ prec).
+ ring_simplify (prec + (emax - prec))%Z.
+ unfold FLT_exp.
+-rewrite Zmax_l.
+-apply Zle_refl.
++rewrite Z.max_l.
++apply Z.le_refl.
+ unfold emin.
+ generalize Hprec' Hemax' ; clear ; omega.
+-rewrite <- abs_IZR, Zabs_eq, <- 2!IZR_Zpower.
++rewrite <- abs_IZR, Z.abs_eq, <- 2!IZR_Zpower.
+ split.
+ apply IZR_le.
+ apply Zlt_succ_le.
+-change (2 ^ prec - 1)%Z with (Zpred (2^prec))%Z.
++change (2 ^ prec - 1)%Z with (Z.pred (2^prec))%Z.
+ rewrite <- Zsucc_pred.
+ apply lt_IZR.
+ change 2%Z with (radix_val radix2).
+@@ -247,7 +247,7 @@
+ exact Hprec'.
+ generalize Hprec' ; clear ; omega.
+ apply Zlt_succ_le.
+-change (2 ^ prec - 1)%Z with (Zpred (2^prec))%Z.
++change (2 ^ prec - 1)%Z with (Z.pred (2^prec))%Z.
+ rewrite <- Zsucc_pred.
+ change 2%Z with (radix_val radix2).
+ apply Zpower_gt_0.
+@@ -307,7 +307,7 @@
+ ring_simplify (emax+1-1)%Z.
+ rewrite Req_bool_true by easy.
+ unfold FLT_exp, emin.
+-rewrite Zmax_l.
++rewrite Z.max_l.
+ unfold max, F2R; simpl.
+ pattern emax at 1; replace emax with (prec+(emax-prec))%Z by ring.
+ rewrite bpow_plus.
+@@ -332,7 +332,7 @@
+ Proof with auto with typeclass_instances.
+ intros m z Hz.
+ apply round_generic...
+-assert (Zabs z <= max_representable_integer)%Z.
++assert (Z.abs z <= max_representable_integer)%Z.
+ apply Abs_le with (1:=Hz).
+ destruct (Zle_lt_or_eq _ _ H) as [Bz|Bz] ; clear H Hz.
+ apply generic_format_FLT.
+Index: why3/lib/coq/for_drivers/ComputerOfEuclideanDivision.v
+===================================================================
+--- why3.orig/lib/coq/for_drivers/ComputerOfEuclideanDivision.v	2020-03-08 08:42:18.093485748 +0100
++++ why3/lib/coq/for_drivers/ComputerOfEuclideanDivision.v	2020-03-08 08:42:18.093485748 +0100
+@@ -19,7 +19,7 @@
+ 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.
+Index: why3/lib/coq/int/Abs.v
+===================================================================
+--- why3.orig/lib/coq/int/Abs.v	2020-03-08 08:42:18.093485748 +0100
++++ why3/lib/coq/int/Abs.v	2020-03-08 08:42:18.093485748 +0100
+@@ -25,12 +25,12 @@
+   (~ (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 *)
+Index: why3/lib/coq/int/ComputerDivision.v
+===================================================================
+--- why3.orig/lib/coq/int/ComputerDivision.v	2020-03-08 08:42:18.093485748 +0100
++++ why3/lib/coq/int/ComputerDivision.v	2020-03-08 08:42:18.093485748 +0100
+@@ -40,9 +40,9 @@
+ 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 @@
+   ((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.
+Index: why3/lib/coq/int/EuclideanDivision.v
+===================================================================
+--- why3.orig/lib/coq/int/EuclideanDivision.v	2020-03-08 08:42:18.093485748 +0100
++++ why3/lib/coq/int/EuclideanDivision.v	2020-03-08 08:42:18.093485748 +0100
+@@ -20,8 +20,8 @@
+ 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 @@
+ 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 *)
+Index: why3/lib/coq/int/Exponentiation.v
+===================================================================
+--- why3.orig/lib/coq/int/Exponentiation.v	2020-03-08 08:42:18.093485748 +0100
++++ why3/lib/coq/int/Exponentiation.v	2020-03-08 08:42:18.093485748 +0100
+@@ -42,7 +42,7 @@
+ (* 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 @@
+ Proof.
+ intros x n h1.
+ unfold power.
+-fold (Zsucc n).
++fold (Z.succ n).
+ now rewrite Zabs_nat_Zsucc.
+ Qed.
+ 
+@@ -88,7 +88,7 @@
+ 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 @@
+ 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 @@
+ 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 @@
+ 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.
+Index: why3/lib/coq/int/Int.v
+===================================================================
+--- why3.orig/lib/coq/int/Int.v	2020-03-08 08:42:18.093485748 +0100
++++ why3/lib/coq/int/Int.v	2020-03-08 08:42:18.093485748 +0100
+@@ -123,14 +123,14 @@
+ 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 *)
+Index: why3/lib/coq/int/MinMax.v
+===================================================================
+--- why3.orig/lib/coq/int/MinMax.v	2020-03-08 08:42:18.093485748 +0100
++++ why3/lib/coq/int/MinMax.v	2020-03-08 08:42:49.989669005 +0100
+@@ -19,15 +19,15 @@
+ (* min is replaced with (ZArith.BinInt.Z.min x x1) by the coq driver *)
+ 
+ (* Why3 goal *)
+-Lemma min_def :
+-  forall (x:Z) (y:Z),
++Lemma min'def :
++  forall (x:Numbers.BinNums.Z) (y:Numbers.BinNums.Z),
+   ((x <= y)%Z -> ((ZArith.BinInt.Z.min x y) = x)) /\
+   (~ (x <= y)%Z -> ((ZArith.BinInt.Z.min x y) = y)).
+ 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.
+ 
+@@ -35,59 +35,63 @@
+ (* max is replaced with (ZArith.BinInt.Z.max x x1) by the coq driver *)
+ 
+ (* Why3 goal *)
+-Lemma max_def :
+-  forall (x:Z) (y:Z),
++Lemma max'def :
++  forall (x:Numbers.BinNums.Z) (y:Numbers.BinNums.Z),
+   ((x <= y)%Z -> ((ZArith.BinInt.Z.max x y) = y)) /\
+   (~ (x <= y)%Z -> ((ZArith.BinInt.Z.max x y) = x)).
+ 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.
++  forall (x:Numbers.BinNums.Z) (y:Numbers.BinNums.Z), (y <= x)%Z ->
++  ((ZArith.BinInt.Z.min x y) = y).
++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.
++  forall (x:Numbers.BinNums.Z) (y:Numbers.BinNums.Z), (y <= x)%Z ->
++  ((ZArith.BinInt.Z.max x y) = x).
++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.
++  forall (x:Numbers.BinNums.Z) (y:Numbers.BinNums.Z),
++  ((ZArith.BinInt.Z.min x y) = (ZArith.BinInt.Z.min y x)).
++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.
++  forall (x:Numbers.BinNums.Z) (y:Numbers.BinNums.Z),
++  ((ZArith.BinInt.Z.max x y) = (ZArith.BinInt.Z.max y x)).
++exact Z.max_comm.
+ Qed.
+ 
+ (* Why3 goal *)
+ Lemma Min_assoc :
+-  forall (x:Z) (y:Z) (z:Z),
++  forall (x:Numbers.BinNums.Z) (y:Numbers.BinNums.Z) (z:Numbers.BinNums.Z),
+   ((ZArith.BinInt.Z.min (ZArith.BinInt.Z.min x y) z) =
+    (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 *)
+ Lemma Max_assoc :
+-  forall (x:Z) (y:Z) (z:Z),
++  forall (x:Numbers.BinNums.Z) (y:Numbers.BinNums.Z) (z:Numbers.BinNums.Z),
+   ((ZArith.BinInt.Z.max (ZArith.BinInt.Z.max x y) z) =
+    (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.
+ 
+Index: why3/lib/coq/int/NumOf.v
+===================================================================
+--- why3.orig/lib/coq/int/NumOf.v	2020-03-08 08:42:18.093485748 +0100
++++ why3/lib/coq/int/NumOf.v	2020-03-08 08:42:18.093485748 +0100
+@@ -50,8 +50,8 @@
+   rewrite <- Z2Nat.inj_pred.
+   simpl numof_aux.
+   rewrite Z2Nat.id by omega.
+-  replace (a + Zpred (b - a))%Z with (b - 1)%Z by (unfold Zpred ; ring).
+-  replace (Zpred (b - a)) with (b - 1 - a)%Z by (unfold Zpred ; ring).
++  replace (a + Z.pred (b - a))%Z with (b - 1)%Z by (unfold Z.pred ; ring).
++  replace (Z.pred (b - a)) with (b - 1 - a)%Z by (unfold Z.pred ; ring).
+   split ; intros h2.
+   rewrite h2.
+   apply Zplus_comm.
+Index: why3/lib/coq/int/Power.v
+===================================================================
+--- why3.orig/lib/coq/int/Power.v	2020-03-08 08:42:18.093485748 +0100
++++ why3/lib/coq/int/Power.v	2020-03-08 08:42:18.093485748 +0100
+@@ -46,7 +46,7 @@
+ 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 @@
+   ((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 *)
+Index: why3/lib/coq/map/MapInjection.v
+===================================================================
+--- why3.orig/lib/coq/map/MapInjection.v	2020-03-08 08:42:18.093485748 +0100
++++ why3/lib/coq/map/MapInjection.v	2020-03-08 08:42:18.093485748 +0100
+@@ -166,10 +166,10 @@
+       forall i:nat, Z_of_nat i < n -> Z_of_nat (g i) = f (Z_of_nat i).
+ Proof.
+ intros n f Hpos.
+-exists (fun n => Zabs_nat (f (Z_of_nat n))).
++exists (fun n => Z.abs_nat (f (Z_of_nat n))).
+ intros i Hi_inf_n.
+ rewrite inj_Zabs_nat.
+-rewrite Zabs_eq; auto.
++rewrite Z.abs_eq; auto.
+ generalize (Hpos (Z_of_nat i)); auto with *.
+ Qed.
+ 
+Index: why3/lib/coq/map/Occ.v
+===================================================================
+--- why3.orig/lib/coq/map/Occ.v	2020-03-08 08:42:18.093485748 +0100
++++ why3/lib/coq/map/Occ.v	2020-03-08 08:42:18.093485748 +0100
+@@ -42,7 +42,7 @@
+ destruct (u - l)%Z ; try easy.
+ simpl.
+ assert (exists n, Pos.to_nat p = S n) as [n ->].
+-  exists (Z.to_nat (Zpred (Zpos p))).
++  exists (Z.to_nat (Z.pred (Zpos p))).
+   rewrite Z2Nat.inj_pred.
+   apply (S_pred _ O).
+   apply Pos2Nat.is_pos.
+Index: why3/lib/coq/number/Divisibility.v
+===================================================================
+--- why3.orig/lib/coq/number/Divisibility.v	2020-03-08 08:42:18.093485748 +0100
++++ why3/lib/coq/number/Divisibility.v	2020-03-08 08:42:18.093485748 +0100
+@@ -29,7 +29,7 @@
+ *)
+ 
+ Require Import Znumtheory.
+-Notation divides := Zdivide (only parsing).
++Notation divides := Z.divide (only parsing).
+ 
+ (* Why3 goal *)
+ Lemma divides_spec :
+@@ -42,7 +42,7 @@
+ (* Why3 goal *)
+ Lemma divides_refl : forall (n:Z), divides n n.
+ Proof.
+-exact Zdivide_refl.
++exact Z.divide_refl.
+ Qed.
+ 
+ (* Why3 goal *)
+@@ -152,14 +152,14 @@
+   forall (a:Z) (b:Z), (divides a b) -> (divides b a) ->
+   (a = b) \/ (a = (-b)%Z).
+ Proof.
+-exact Zdivide_antisym.
++exact Z.divide_antisym.
+ Qed.
+ 
+ (* Why3 goal *)
+ Lemma divides_trans :
+   forall (a:Z) (b:Z) (c:Z), (divides a b) -> (divides b c) -> divides a c.
+ Proof.
+-exact Zdivide_trans.
++exact Z.divide_trans.
+ Qed.
+ 
+ (* Why3 goal *)
+Index: why3/lib/coq/number/Gcd.v
+===================================================================
+--- why3.orig/lib/coq/number/Gcd.v	2020-03-08 08:42:18.093485748 +0100
++++ why3/lib/coq/number/Gcd.v	2020-03-08 08:42:18.093485748 +0100
+@@ -23,7 +23,7 @@
+ Import Znumtheory.
+ 
+ (* Why3 goal *)
+-Notation gcd := Zgcd (only parsing).
++Notation gcd := Z.gcd (only parsing).
+ 
+ (* Why3 goal *)
+ Lemma gcd_nonneg : forall (a:Z) (b:Z), (0%Z <= (gcd a b))%Z.
+@@ -80,14 +80,14 @@
+ (* Why3 goal *)
+ Lemma Comm : forall (x:Z) (y:Z), ((gcd x y) = (gcd y x)).
+ Proof.
+-exact Zgcd_comm.
++exact Z.gcd_comm.
+ Qed.
+ 
+ (* Why3 goal *)
+ Lemma gcd_0_pos : forall (a:Z), (0%Z <= a)%Z -> ((gcd a 0%Z) = a).
+ Proof.
+ intros a H.
+-rewrite <- (Zabs_eq a H) at 2.
++rewrite <- (Z.abs_eq a H) at 2.
+ apply Zgcd_0.
+ Qed.
+ 
+@@ -129,7 +129,7 @@
+   ((gcd b (ZArith.BinInt.Z.rem a b)) = (gcd a b)).
+ Proof.
+ intros a b _.
+-rewrite (Zgcd_comm a b).
++rewrite (Z.gcd_comm a b).
+ rewrite (gcd_euclid b a (Z.quot a b)).
+ apply f_equal.
+ rewrite (Z.quot_rem' a b) at 2.
+@@ -142,7 +142,7 @@
+   ((gcd b (int.EuclideanDivision.mod1 a b)) = (gcd a b)).
+ Proof.
+ intros a b Zb.
+-rewrite (Zgcd_comm a b).
++rewrite (Z.gcd_comm a b).
+ rewrite (gcd_euclid b a (EuclideanDivision.div a b)).
+ apply f_equal.
+ rewrite (EuclideanDivision.Div_mod a b Zb) at 2.
+Index: why3/lib/coq/number/Prime.v
+===================================================================
+--- why3.orig/lib/coq/number/Prime.v	2020-03-08 08:42:18.093485748 +0100
++++ why3/lib/coq/number/Prime.v	2020-03-08 08:42:18.093485748 +0100
+@@ -82,7 +82,7 @@
+ exact Pp.
+ elimtype False.
+ (* *)
+-assert (exists d, (2 <= d)%Z /\ (d * d <= p)%Z /\ prime d /\ Zdivide d p).
++assert (exists d, (2 <= d)%Z /\ (d * d <= p)%Z /\ prime d /\ Z.divide d p).
+ clear H.
+ assert (Hp' : (0 <= p)%Z) by omega.
+ revert p Hp' Hp Pp.
+@@ -107,13 +107,13 @@
+ exact Px.
+ exists y.
+ refine (conj Hy1 (conj _ (conj Hy3 _))).
+-apply Zle_trans with (1 := Hy2).
+-apply Zle_trans with (2 := Hx).
++apply Z.le_trans with (1 := Hy2).
++apply Z.le_trans with (2 := Hx).
+ rewrite <- (Zmult_1_r x) at 1.
+ apply Zmult_le_compat_l.
+ now apply Zlt_le_weak.
+ clear -Hx1 ; omega.
+-now apply Zdivide_trans with x.
++now apply Z.divide_trans with x.
+ case Hx2.
+ intros q Hq1.
+ assert (Hq2 : (2 <= q)%Z).
+@@ -148,18 +148,18 @@
+ exact Pq.
+ exists y.
+ refine (conj Hy1 (conj _ (conj Hy3 _))).
+-apply Zle_trans with (1 := Hy2).
++apply Z.le_trans with (1 := Hy2).
+ rewrite <- (Zmult_1_r q), Hq1.
+ apply Zmult_le_compat_l.
+ clear -Hx1 ; omega.
+ clear -Hq2 ; omega.
+-apply Zdivide_trans with (1 := Hy4).
++apply Z.divide_trans with (1 := Hy4).
+ exists x.
+ now rewrite Zmult_comm.
+ destruct H0 as (y&Hy1&Hy2&Hy3&Hy4).
+ apply (H y) ; try easy.
+ split.
+-apply Zlt_le_trans with (2 * 2)%Z.
++apply Z.lt_le_trans with (2 * 2)%Z.
+ easy.
+ now apply Zmult_le_compat.
+ exact Hy2.
+@@ -171,7 +171,7 @@
+ Proof.
+ intros p Pp (q,Hq).
+ generalize (proj2 Pp q).
+-assert (Zdivide q p).
++assert (Z.divide q p).
+ now exists 2%Z.
+ intros.
+ refine (_ (fun H1 => H0 H1 H) (proj1 Pp)).
+Index: why3/lib/coq/real/Truncate.v
+===================================================================
+--- why3.orig/lib/coq/real/Truncate.v	2020-03-08 08:42:18.093485748 +0100
++++ why3/lib/coq/real/Truncate.v	2020-03-08 08:42:18.093485748 +0100
+@@ -18,7 +18,7 @@
+ Require real.FromInt.
+ 
+ Require Import Flocq.Core.Core.
+-Require Import Fourier.
++Require Import Lra.
+ 
+ (* Why3 goal *)
+ Notation truncate := Ztrunc.
+@@ -54,12 +54,12 @@
+   split;[|apply Zceil_ub].
+   case (Req_dec (IZR (Zfloor x)) x); intro.
+   rewrite <-H, Zceil_IZR, H, minus_IZR; simpl.
+-  fourier.
++  lra.
+   rewrite (Zceil_floor_neq _ H).
+   rewrite minus_IZR, plus_IZR; simpl.
+   pose proof (Zfloor_lb x).
+   destruct (Rle_lt_or_eq_dec _ _ H0); try easy.
+-  fourier.
++  lra.
+ Qed.
+ 
+ (* Why3 goal *)
+@@ -72,15 +72,15 @@
+   destruct (Rle_lt_dec x 0).
+   + rewrite Ztrunc_ceil; auto.
+     destruct (Req_dec (IZR (Zfloor x)) x).
+-    rewrite <-H at 2 3; rewrite Zceil_IZR, H; split; fourier.
++    rewrite <-H at 2 3; rewrite Zceil_IZR, H; split; lra.
+     rewrite Zceil_floor_neq; auto.
+     pose proof (Zfloor_lb x);
+       pose proof (Zfloor_ub x).
+-    rewrite plus_IZR; split; fourier.
+-  + rewrite Ztrunc_floor by fourier.
++    rewrite plus_IZR; split; lra.
++  + rewrite Ztrunc_floor by lra.
+     pose proof (Zfloor_lb x);
+       pose proof (Zfloor_ub x).
+-    split; fourier.
++    split; lra.
+ Qed.
+ 
+ (* Why3 goal *)
+@@ -98,7 +98,7 @@
+   destruct (Rle_lt_dec x 0).
+   + rewrite Ztrunc_ceil; auto.
+     apply Zceil_glb; assumption.
+-  + rewrite Ztrunc_floor by fourier.
++  + rewrite Ztrunc_floor by lra.
+     apply le_IZR.
+     apply Rle_trans with (r2:=x);[apply Zfloor_lb|assumption].
+ Qed.
+@@ -112,7 +112,7 @@
+   + rewrite Ztrunc_ceil; auto.
+     apply le_IZR.
+     apply Rle_trans with (r2:=x);[assumption|apply Zceil_ub].
+-  + rewrite Ztrunc_floor by fourier.
++  + rewrite Ztrunc_floor by lra.
+     apply Zfloor_lub; assumption.
+ Qed.
+ 
+@@ -147,16 +147,16 @@
+   apply Zfloor_ub.
+ Qed.
+ 
+-Lemma ceil_lb: forall x, ((IZR (ceil x) - 1) < x).
++Lemma ceil_lb: forall x, ((IZR (ceil x) - 1) < x)%R.
+ Proof.
+   intro.
+   case (Req_dec (IZR (Zfloor x)) x); intro.
+-  rewrite <-H, Zceil_IZR, H; simpl; fourier.
++  rewrite <-H, Zceil_IZR, H; simpl; lra.
+   rewrite (Zceil_floor_neq _ H).
+   rewrite plus_IZR; simpl.
+   pose proof (Zfloor_lb x).
+   destruct (Rle_lt_or_eq_dec _ _ H0); try easy.
+-  fourier.
++  lra.
+ Qed.
+ 
+ (* Why3 goal *)
diff -Nru why3-1.2.1/debian/patches/series why3-1.2.1/debian/patches/series
--- why3-1.2.1/debian/patches/series	2020-02-10 12:57:51.000000000 +0000
+++ why3-1.2.1/debian/patches/series	2020-03-08 19:36:59.000000000 +0000
@@ -1,2 +1,3 @@
 hardening-flags
 0002-Move-menhirLib-from-EXTOBJS-to-EXTLIBS.patch
+coq-8.10+11
diff -Nru why3-1.2.1/debian/rules why3-1.2.1/debian/rules
--- why3-1.2.1/debian/rules	2020-02-10 12:57:51.000000000 +0000
+++ why3-1.2.1/debian/rules	2020-03-08 19:36:59.000000000 +0000
@@ -1,7 +1,12 @@
 #!/usr/bin/make -f
 
 BUILDDIR=debian/tmp
-include /usr/share/coq/coqvars.mk
+
+HAVE_COQVARS ?= $(if $(wildcard /usr/share/coq/coqvars.mk),yes,no)
+
+ifeq ($(HAVE_COQVARS),yes)
+  include /usr/share/coq/coqvars.mk
+endif
 
 %:
 	dh $@ --with ocaml,tex
@@ -9,6 +14,7 @@
 override_dh_auto_configure: configure-stamp
 
 configure-stamp:
+	autoconf
 	dh_auto_configure -- \
 		--disable-emacs-compilation
 	touch configure-stamp
@@ -29,7 +35,9 @@
 override_dh_install-arch: build-arch
 	$(MAKE) install install-lib DESTDIR=$(CURDIR)/$(BUILDDIR)
 	dh_install -a -XLICENSE
+ifeq ($(HAVE_COQVARS),yes)
 	echo 'F:CoqABI=$(COQ_ABI)' >> debian/why3-coq.substvars
+endif
 
 override_dh_installexamples:
 	dh_installexamples
@@ -51,6 +59,3 @@
 
 override_dh_ocaml:
 	dh_ocaml --nodefined-map=why3-coq:Why3,MenhirLib,Gzip,Zlib,Zip \
-		--nodefined-map=why3:Graph
-override_dh_dwz:
-	dh_dwz --no-dwz-multifile
diff -Nru why3-1.2.1/debian/tests/control why3-1.2.1/debian/tests/control
--- why3-1.2.1/debian/tests/control	2020-02-10 12:57:51.000000000 +0000
+++ why3-1.2.1/debian/tests/control	2020-03-08 19:36:59.000000000 +0000
@@ -16,3 +16,4 @@
 
 Tests: why3+coq
 Depends: why3, why3-coq, coq
+Restrictions: skip-not-installable