diff --git a/sources b/sources
index 99a1865..f503a9e 100644
--- a/sources
+++ b/sources
@@ -1 +1 @@
-SHA512 (why3-1.8.0.tar.gz) = 8d30ac4a1280a7d7741ef862365e06aa3218a78fd01ca7f969f0d6515245c7259fcc81897bfe08c581c6b37639d1465ab4a96657f3baf4c747988df8201d4549
+SHA512 (why3-1.8.2.tar.gz) = a35e88fafe1aa29c36d2248c1a644eae85afa1bb7b3009193f4a5c28ba684d0882717d63733d8581a7c2cd5ec493e2d15c82baabef615b4d00323fa9309875f8
diff --git a/why3-c23.patch b/why3-c23.patch
deleted file mode 100644
index 736756b..0000000
--- a/why3-c23.patch
+++ /dev/null
@@ -1,25 +0,0 @@
-Fixes this error:
-
-src/server/cpulimit-unix.c: In function ‘main’:
-src/server/cpulimit-unix.c:95:23: error: assignment to ‘__sighandler_t’ {aka ‘void (*)(int)’} from incompatible pointer type ‘void (*)(void)’ [-Wincompatible-pointer-types]
-   95 |         sa.sa_handler = &wallclock_timelimit_reached;
-      |                       ^
-src/server/cpulimit-unix.c:45:6: note: ‘wallclock_timelimit_reached’ declared here
-   45 | void wallclock_timelimit_reached() {
-      |      ^~~~~~~~~~~~~~~~~~~~~~~~~~~
-In file included from src/server/cpulimit-unix.c:22:
-/usr/include/signal.h:72:16: note: ‘__sighandler_t’ declared here
-   72 | typedef void (*__sighandler_t) (int);
-      |                ^~~~~~~~~~~~~~
-
---- why3-1.8.0/src/server/cpulimit-unix.c.orig	2024-12-11 06:21:37.000000000 -0700
-+++ why3-1.8.0/src/server/cpulimit-unix.c	2025-01-22 14:48:28.808369208 -0700
-@@ -42,7 +42,7 @@ void show_time() {
-   }
- }
- 
--void wallclock_timelimit_reached() {
-+void wallclock_timelimit_reached([[maybe_unused]] int sig) {
-   fprintf(stderr,
-           "Why3cpulimit: wallclock timelimit %d reached, killing command\n",
-           wallclock_timelimit);
diff --git a/why3-link-order.patch b/why3-link-order.patch
deleted file mode 100644
index 25cfeec..0000000
--- a/why3-link-order.patch
+++ /dev/null
@@ -1,20 +0,0 @@
-Fixes this error:
-
-File "_none_", line 1:
-Error: Forward reference to "Ptree_helpers" in file "src/bddinfer/why3infer.cmo"
-
---- why3-1.8.0/Makefile.in.orig	2024-12-11 06:21:37.000000000 -0700
-+++ why3-1.8.0/Makefile.in	2024-12-16 10:27:14.100846332 -0700
-@@ -318,10 +318,10 @@ LIBMODULES =  $(addprefix src/util/, $(L
- 	      $(addprefix src/core/, $(LIB_CORE)) \
- 	      $(addprefix src/driver/, $(LIB_DRIVER)) \
- 	      $(addprefix src/mlw/, $(LIB_MLW)) \
--	      $(addprefix src/infer/, $(LIB_INFER)) \
--	      $(addprefix src/bddinfer/, $(LIB_BDDINFER)) \
- 	      $(addprefix src/extract/, $(LIB_EXTRACT)) \
- 	      $(addprefix src/parser/, $(LIB_PARSER)) \
-+	      $(addprefix src/infer/, $(LIB_INFER)) \
-+	      $(addprefix src/bddinfer/, $(LIB_BDDINFER)) \
- 	      $(addprefix src/transform/, $(LIB_TRANSFORM)) \
- 	      $(addprefix src/printer/, $(LIB_PRINTER)) \
- 	      $(addprefix src/session/, $(LIB_SESSION))
diff --git a/why3-rocq-9.2.patch b/why3-rocq-9.2.patch
new file mode 100644
index 0000000..9b2042c
--- /dev/null
+++ b/why3-rocq-9.2.patch
@@ -0,0 +1,292 @@
+--- why3-1.8.2/lib/coq/ieee_float/GenericFloat.v.orig	2025-09-16 09:37:32.000000000 -0600
++++ why3-1.8.2/lib/coq/ieee_float/GenericFloat.v	2026-04-12 21:00:50.656964191 -0600
+@@ -476,7 +476,7 @@ Qed.
+ 
+ Lemma is_nan_dec: forall x, {is_nan x} + {~ is_nan x}.
+ Proof.
+-  intro; destruct x; compute; intuition.
++  intro; destruct x; compute; intuition; auto with *.
+ Qed.
+ 
+ Lemma eq_not_nan_refl: forall {x : t}, ~ is_nan x -> eq x x.
+--- why3-1.8.2/lib/coq/map/Occ.v.orig	2025-09-16 09:37:32.000000000 -0600
++++ why3-1.8.2/lib/coq/map/Occ.v	2026-04-12 20:11:22.595468204 -0600
+@@ -241,10 +241,10 @@ now rewrite occ_empty; lia.
+ destruct (why_decidable_eq (m (l + (x-1))%Z) v).
+ assert (m (l + (x - 1)) <> v)%Z.
+   apply H1; lia.
+-intuition.
++intuition; auto with *.
+ rewrite occ_right_no_add.
+ replace (l+x-1)%Z with (l+(x-1))%Z by ring.
+-apply H; intuition.
++apply H; intuition; auto with *.
+ apply (H1 i). lia. assumption.
+ lia.
+ replace (l + x - 1)%Z with (l+(x-1))%Z by ring.
+--- why3-1.8.2/lib/coq/number/Prime.v.orig	2025-09-16 09:37:32.000000000 -0600
++++ why3-1.8.2/lib/coq/number/Prime.v	2026-04-11 14:50:08.453344009 -0600
+@@ -34,6 +34,8 @@ intros p.
+ apply iff_trans with (2 := prime_alt p).
+ unfold prime, prime'.
+ intuition.
++lia.
++lia.
+ Qed.
+ 
+ (* Why3 goal *)
+--- why3-1.8.2/lib/coq/set/Cardinal.v.orig	2025-09-16 09:37:32.000000000 -0600
++++ why3-1.8.2/lib/coq/set/Cardinal.v	2026-04-11 20:38:44.347517956 -0600
+@@ -165,9 +165,10 @@ destruct (Bool.bool_dec (s x) true) as [
+ + exists (List.cons x l1).
+   split.
+   - constructor; auto. intro Habs. eapply h1 in Habs. unfold Map.set in Habs. 
+-    destruct why_decidable_eq; intuition.
++    destruct why_decidable_eq; auto with *.
+   - unfold Map.set in h1. intros. specialize (h1 e). destruct why_decidable_eq; [| intuition]. subst.
+-    split; intuition. destruct H1; eauto.
++    split; auto with *. destruct H1; eauto.
++    auto with *.
+ + exists l1.
+   split; [auto|]. intros. specialize (h1 e). replace (Map.set s x false e) with (s e) in h1.
+   eauto.
+@@ -184,12 +185,15 @@ induction l.
+ - destruct IHl. destruct H.
+   destruct (List.in_dec eq_dec a l). 
+   + exists x. split; eauto. intros. rewrite H0.
+-    split; intuition. inversion H2; eauto. subst. assumption.
++    split; auto with *; intuition. apply List.in_cons. assumption.
++    inversion H2; eauto. subst. assumption.
+   + destruct (Pdec a). 
+     ++ exists (List.cons a x). split. constructor; eauto.
+        rewrite H0. intro Habs. destruct Habs; eauto.
+        intros. simpl. rewrite H0. intuition. subst. assumption.
+-    ++ exists x. split; eauto. intros. rewrite H0. intuition. simpl in H2. destruct H2; try subst; intuition. 
++    ++ exists x. split; eauto. intros. rewrite H0. auto with *; intuition.
++       apply List.in_cons. assumption.
++       simpl in H2. destruct H2; try subst; intuition. 
+ Qed.
+ 
+ (* Why3 goal *)
+@@ -443,7 +447,7 @@ split; intros.
+       + eapply List.NoDup_incl_length; eauto. apply a0. intros e Hincl. eapply H2. assumption.
+       + eapply List.NoDup_incl_length; eauto. intros e Hincl. eapply H2. assumption.
+     }
+-    intuition.
++    intuition. auto with *.
+   }
+   rewrite Hnat. rewrite Nat2Z.inj_succ. ring. 
+ Qed.
+@@ -472,6 +476,7 @@ split.
+   assert (~ set.Set.mem x s'). 
+   { unfold s'. unfold Map.set, set.Set.mem.
+     destruct why_decidable_eq; intuition. 
++    discriminate H1.
+   }
+   eapply cardinal_add in H1. rewrite H1. ring.
+   unfold s'. eapply is_finite_remove. assumption.
+--- why3-1.8.2/lib/coq/set/FsetInt.v.orig	2025-09-16 09:37:32.000000000 -0600
++++ why3-1.8.2/lib/coq/set/FsetInt.v	2026-04-12 12:49:09.882660225 -0600
+@@ -127,8 +127,8 @@ Fixpoint seqZ l len : list Numbers.BinNu
+ 
+ Lemma seqZ_le: forall len x l, List.In x (seqZ l len) -> (l <= x)%Z.
+ Proof.
+-induction len; simpl; intuition.
+-eapply IHlen in H0; intuition.
++induction len; simpl; intuition. auto with *.
++eapply IHlen in H0; intuition. auto with *.
+ Qed.
+ 
+ Lemma seqZ_le2: forall len x l, List.In x (seqZ l len) -> (x < l + Z.of_nat len)%Z.
+@@ -184,8 +184,9 @@ destruct (Z_le_dec l r).
+     destruct Z_le_dec.
+     * destruct Z_lt_dec. split; intros; [reflexivity|].
+       intuition.
+-      intuition ; try inversion H.
+-    * intuition ; try inversion H.
++      intuition ; auto with *; try inversion H.
++      intuition ; auto with *; try inversion H.
++    * intuition ; auto with *; try inversion H.
+ + exists List.nil. 
+   split.
+   - constructor.
+@@ -230,9 +231,10 @@ destruct (Z_le_dec l r).
+   split. apply seqZ_NoDup.
+   intros. rewrite seqZ_In_iff.
+   rewrite Z2Nat.id; [|lia].
+-  destruct Z_le_dec; try destruct Z_lt_dec; intuition; try inversion H.
++  destruct Z_le_dec; try destruct Z_lt_dec; intuition; auto with *; try inversion H.
+ + exists nil. split. constructor.
+   simpl. intros. destruct Z_le_dec; try destruct Z_lt_dec; intuition.
++  auto with *. auto with *. auto with *.
+ Qed.
+ 
+ 
+@@ -265,6 +267,6 @@ split.
+ + intros. destruct a. 
+   destruct x. reflexivity.
+   specialize (H2 z). contradict H2. destruct Z_le_dec. 
+-  destruct Z_lt_dec. lia. intuition. intuition.
++  destruct Z_lt_dec. lia. intuition; auto with *. intuition; auto with *.
+ Qed.
+ 
+--- why3-1.8.2/lib/coq/set/FsetSum.v.orig	2025-09-16 09:37:32.000000000 -0600
++++ why3-1.8.2/lib/coq/set/FsetSum.v	2026-04-12 13:20:34.237382880 -0600
+@@ -101,8 +101,8 @@ destruct ClassicalEpsilon.constructive_i
+ destruct a0 as (Hx0dup, Hx0eq). destruct a1 as (Hx1dup, Hx1eq).
+ split. intros.
+ + eapply fold_left_iff_symm; eauto.
+-  * intuition.
+-  * intuition.
++  * intuition; auto with *.
++  * intuition; auto with *.
+   * intros. rewrite Hx0eq. rewrite Hx1eq. unfold Map.set. 
+     destruct why_decidable_eq; try subst; intuition.
+ + intros.
+@@ -113,19 +113,19 @@ split. intros.
+   erewrite <- (fold_left_iff_symm (List.app x0' x0'')); eauto.
+   * rewrite List.fold_left_app. rewrite fold_left_symm.
+     ++ auto.
+-    ++ intuition.
+-    ++ intuition.
+-  * intuition.
+-  * intuition.
++    ++ intuition; auto with *.
++    ++ intuition; auto with *.
++  * intuition; auto with *.
++  * intuition; auto with *.
+   * intros. rewrite List.in_app_iff. rewrite Hx0 in Hx0eq.
+     specialize (Hx0eq e). rewrite List.in_app_iff in Hx0eq. simpl in Hx0eq.
+     unfold Map.set in *. split; intros.
+     ++ destruct H2.
+        ** apply Hx1eq. destruct why_decidable_eq.
+-          -- subst. eapply List.NoDup_remove_2 in Hx0dup. intuition.
++          -- subst. eapply List.NoDup_remove_2 in Hx0dup. intuition; auto with *.
+           -- intuition.
+        ** eapply Hx1eq. destruct why_decidable_eq.
+-          -- subst. eapply List.NoDup_remove_2 in Hx0dup. intuition.
++          -- subst. eapply List.NoDup_remove_2 in Hx0dup. intuition; auto with *.
+           -- intuition.
+     ++ eapply Hx1eq in H2.
+        destruct why_decidable_eq.
+@@ -177,11 +177,11 @@ destruct ClassicalEpsilon.constructive_i
+ destruct a1 as (Hdidup, Hdieq).
+ destruct a0 as (Hx0dup, Hx0eq).
+ destruct a2 as (Hx1dup, Hx1eq).
+-  rewrite fold_left_symm; try now intuition.
++  rewrite fold_left_symm; try now intuition; auto with *.
+   rewrite Z.add_0_l. rewrite <- List.fold_left_app.
+   eapply fold_left_iff_symm; eauto.
+-  + intuition.
+-  + intuition.
++  + intuition; auto with *.
++  + intuition; auto with *.
+   + intros. rewrite List.in_app_iff. rewrite Hx1eq. rewrite Hx0eq.
+     rewrite Hdieq. rewrite set.Set.diff'def. unfold set.Set.mem.
+     split; intros.
+@@ -210,11 +210,11 @@ destruct ClassicalEpsilon.constructive_i
+ destruct a0 as (Hundup, Huneq).
+ destruct a1 as (Hx0dup, Hx0eq).
+ destruct a2 as (Hx1dup, Hx1eq).
+-  rewrite fold_left_symm; try now intuition.
++  rewrite fold_left_symm; try now intuition; auto with *.
+   rewrite Z.add_0_l. rewrite <- List.fold_left_app.
+   eapply fold_left_iff_symm; eauto.
+-  + intuition.
+-  + intuition.
++  + intuition; auto with *.
++  + intuition; auto with *.
+   + intros. rewrite List.in_app_iff. rewrite Hx1eq. rewrite Hx0eq. rewrite Huneq.
+     rewrite set.Set.union'def. clear - e. intuition.
+   + eapply Cardinal.NoDup_app; eauto.
+@@ -312,7 +312,7 @@ assert (Z.of_nat (length (a0 :: x)) = Z.
+ simpl. rewrite Zpos_P_of_succ_nat. ring.
+ rewrite H.
+ rewrite IHx. rewrite @fold_left_symm; eauto.
+-intuition.
+-intuition.
++intuition; auto with *.
++intuition; auto with *.
+ Qed.
+ 
+--- why3-1.8.2/lib/coq/set/Fset.v.orig	2025-09-16 09:37:32.000000000 -0600
++++ why3-1.8.2/lib/coq/set/Fset.v	2026-04-11 21:14:24.563998083 -0600
+@@ -103,12 +103,14 @@ Proof.
+ exists (fun x => false). 
+ apply Cardinal.is_finite_empty. unfold set.Set.is_empty.
+ unfold set.Set.mem. intuition.
++discriminate H.
+ Defined.
+ 
+ (* Why3 goal *)
+ Lemma is_empty_empty {a:Type} {a_WT:WhyType a} : is_empty (empty : fset a).
+ Proof.
+ unfold empty, is_empty, mem, set.Set.mem. intuition.
++discriminate H.
+ Qed.
+ 
+ (* Why3 goal *)
+@@ -118,6 +120,7 @@ Proof.
+ intros s h1.
+ eapply extensionality. intro. unfold empty, is_empty, mem, set.Set.mem in *.
+ destruct s. intuition. destruct (h1 _ H). 
++discriminate H.
+ Qed.
+ 
+ (* Why3 goal *)
+@@ -163,6 +166,7 @@ Proof.
+ intros x s y.
+ unfold mem, remove, set.Set.mem, Map.set. destruct s.
+ destruct why_decidable_eq; intuition.
++discriminate H. discriminate H.
+ Qed.
+ 
+ (* Why3 goal *)
+--- why3-1.8.2/lib/coq/set/SetImpInt.v.orig	2025-09-16 09:37:32.000000000 -0600
++++ why3-1.8.2/lib/coq/set/SetImpInt.v	2026-04-12 13:35:37.131334141 -0600
+@@ -48,6 +48,6 @@ Lemma choose'spec :
+ Proof.
+ intros s h1.
+ destruct h1. unfold to_fset, Fset.is_empty, Fset.mem, set.Set.mem.
+-intuition.
++intuition. inversion H.
+ Qed.
+ 
+--- why3-1.8.2/lib/coq/set/SetImp.v.orig	2025-09-16 09:37:32.000000000 -0600
++++ why3-1.8.2/lib/coq/set/SetImp.v	2026-04-12 13:28:53.584021692 -0600
+@@ -53,6 +53,6 @@ Lemma choose'spec :
+ Proof.
+ intros s h1.
+ destruct h1. unfold to_fset, Fset.is_empty, Fset.mem, set.Set.mem.
+-intuition.
++intuition. inversion H.
+ Qed.
+ 
+--- why3-1.8.2/lib/coq/set/Set.v.orig	2025-09-16 09:37:32.000000000 -0600
++++ why3-1.8.2/lib/coq/set/Set.v	2026-04-11 15:34:29.297022916 -0600
+@@ -139,6 +139,7 @@ Proof.
+ intros x s y.
+ unfold mem, Map.set.
+ destruct (why_decidable_eq x y) as [->|H] ; intuition.
++discriminate H.
+ Qed.
+ 
+ (* Why3 goal *)
+@@ -332,7 +333,7 @@ intuition.
+   destruct (s1 x); destruct (s2 x); intuition.
+ - rewrite <- H.
+   rewrite Bool.andb_true_iff.
+-  destruct (s2 x); intuition.
++  destruct (s2 x); auto with *.
+ Qed.
+ 
+ (* Why3 goal *)
+@@ -345,7 +346,7 @@ unfold disjoint, diff.
+ unfold mem.
+ intros x.
+ rewrite Bool.andb_true_iff.
+-destruct (s2 x); intuition.
++destruct (s2 x); auto with *.
+ Qed.
+ 
+ (* Why3 goal *)
diff --git a/why3-zmod.patch b/why3-zmod.patch
new file mode 100644
index 0000000..48f3ae4
--- /dev/null
+++ b/why3-zmod.patch
@@ -0,0 +1,33 @@
+--- why3-1.8.2/lib/coq/bv/BV_Gen.v.orig	2025-09-16 09:37:32.000000000 -0600
++++ why3-1.8.2/lib/coq/bv/BV_Gen.v	2026-03-03 17:07:31.885655859 -0700
+@@ -994,7 +994,7 @@ match p with
+             ((Vector.last prev) :: (Vector.shiftout prev))
+ end.
+ 
+-Lemma mod1_is_mod : forall x y, y > 0 -> mod1 x y = Zmod x y.
++Lemma mod1_is_mod : forall x y, y > 0 -> mod1 x y = Z.modulo x y.
+   intros; unfold mod1, div.
+   case Z_le_dec; intro.
+   rewrite Z.mod_eq by lia; trivial.
+--- why3-1.8.2/lib/coq/int/EuclideanDivision.v.orig	2025-09-16 09:37:32.000000000 -0600
++++ why3-1.8.2/lib/coq/int/EuclideanDivision.v	2026-03-03 17:08:16.588687381 -0700
+@@ -21,7 +21,7 @@ Require Import Lia.
+ Definition div : Numbers.BinNums.Z -> Numbers.BinNums.Z -> Numbers.BinNums.Z.
+ Proof.
+ intros x y.
+-case (Z_le_dec 0 (Zmod x y)) ; intros H.
++case (Z_le_dec 0 (Z.modulo x y)) ; intros H.
+ exact (Z.div x y).
+ exact (Z.div x y + 1)%Z.
+ Defined.
+--- why3-1.8.2/lib/coq/number/Divisibility.v.orig	2025-09-16 09:37:32.000000000 -0600
++++ why3-1.8.2/lib/coq/number/Divisibility.v	2026-03-03 17:08:33.884500190 -0700
+@@ -203,7 +203,7 @@ Lemma divides_mod_euclidean :
+   divides b a -> ((int.EuclideanDivision.mod1 a b) = 0%Z).
+ Proof.
+ intros a b Zb H.
+-assert (Zmod a b = Z0).
++assert (Z.modulo a b = Z0).
+ now apply Zdivide_mod.
+ unfold mod1, div.
+ rewrite H0.
diff --git a/why3.spec b/why3.spec
index 12b1211..3fc4249 100644
--- a/why3.spec
+++ b/why3.spec
@@ -1,13 +1,10 @@
-# Coq's plugin architecture requires cmxs files, so:
-ExclusiveArch: %{ocaml_native_compiler}
-
 # NOTE: Upstream has said that the Frama-C support is still experimental, and
 # less functional than the corresponding support in why2.  They recommend not
 # enabling it for now.  We abide by their wishes.  Revisit this decision each
 # release.
 
 Name:           why3
-Version:        1.8.0
+Version:        1.8.2
 Release:        %autorelease
 Summary:        Software verification platform
 
@@ -19,16 +16,18 @@ Source0:        https://why3.gitlabpages.inria.fr/releases/%{name}-%{version}.ta
 Source1:        fr.lri.%{name}.desktop
 # AppData file written by Jerry James
 Source2:        fr.lri.%{name}.metainfo.xml
-# Fix a link order issue
-Patch:          %{name}-link-order.patch
-# Fix an incompatible pointer issue with C23
-Patch:          %{name}-c23.patch
+# The deprecated Zmod alias was removed in rocq-stdlib 9.1.0
+Patch:          %{name}-zmod.patch
+# Adapt to changes in rocq 9.2.0
+Patch:          %{name}-rocq-9.2.patch
 
-BuildRequires:  coq
+# Coq's plugin architecture requires cmxs files, so:
+ExclusiveArch:  %{ocaml_native_compiler}
+
+BuildRequires:  coq-core-compat
 BuildRequires:  emacs-nw
 BuildRequires:  emacs-proofgeneral
 BuildRequires:  flocq
-BuildRequires:  graphviz
 BuildRequires:  java-devel
 BuildRequires:  latexmk
 BuildRequires:  libappstream-glib
@@ -41,7 +40,6 @@ BuildRequires:  ocaml-lablgtk3-sourceview3-devel
 BuildRequires:  ocaml-menhir
 BuildRequires:  ocaml-mlmpfr-devel
 BuildRequires:  ocaml-num-devel
-BuildRequires:  ocaml-ocamldoc
 BuildRequires:  ocaml-ocamlgraph-devel
 BuildRequires:  ocaml-ppx-deriving-devel
 BuildRequires:  ocaml-ppx-sexp-conv-devel
@@ -49,19 +47,9 @@ BuildRequires:  ocaml-re-devel
 BuildRequires:  ocaml-sexplib-devel
 BuildRequires:  ocaml-zarith-devel
 BuildRequires:  ocaml-zip-devel
-BuildRequires:  %{py3_dist sphinx}
-BuildRequires:  %{py3_dist sphinxcontrib-bibtex}
-BuildRequires:  tex(capt-of.sty)
-BuildRequires:  tex(comment.sty)
-BuildRequires:  tex(fncychap.sty)
-BuildRequires:  tex(framed.sty)
-BuildRequires:  tex(latex)
-BuildRequires:  tex(needspace.sty)
-BuildRequires:  tex(tabulary.sty)
-BuildRequires:  tex(tgtermes.sty)
-BuildRequires:  tex(upquote.sty)
-BuildRequires:  tex(wrapfig.sty)
-BuildRequires:  tex-urlbst
+BuildRequires:  rocq
+BuildRequires:  texlive-latex
+BuildRequires:  vim-filesystem
 
 Requires:       gtksourceview3%{?_isa}
 Requires:       hicolor-icon-theme
@@ -77,12 +65,12 @@ Provides:       bundled(js-jquery)
 %global __requires_exclude ocaml\\\(Driver_ast\\\)
 
 %description
-Why3 is the next generation of the Why software verification platform.
-Why3 clearly separates the purely logical specification part from
-generation of verification conditions for programs.  It features a rich
-library of proof task transformations that can be chained to produce a
-suitable input for a large set of theorem provers, including SMT
-solvers, TPTP provers, as well as interactive proof assistants.
+Why3 is the next generation of the Why software verification platform.  Why3
+clearly separates the purely logical specification part from generation of
+verification conditions for programs.  It features a rich library of proof
+task transformations that can be chained to produce a suitable input for a
+large set of theorem provers, including SMT solvers, TPTP provers, as well as
+interactive proof assistants.
 
 %package examples
 Summary:        Example inputs
@@ -107,16 +95,16 @@ Requires:       %{name}%{?_isa} = %{version}-%{release}
 Requires:       alt-ergo coq cvc5 E gappa yices-tools z3 zenon
 
 %description all
-This package provides a complete software verification platform suite
-based on Why3, including various automated and interactive provers.
+This package provides a complete software verification platform suite based on
+Why3, including various automated and interactive provers.
 
 %package -n ocaml-%{name}
 Summary:        Software verification library for ocaml
 Requires:       ocaml-zip-devel%{?_isa}
 
 %description -n ocaml-%{name}
-This package contains an ocaml library that exposes the functionality
-of why3 to applications.
+This package contains an ocaml library that exposes the functionality of why3
+to applications.
 
 %package -n ocaml-%{name}-devel
 Summary:        Development files for using the ocaml-%{name} library
@@ -128,8 +116,8 @@ Requires:       ocaml-sexplib-devel%{?_isa}
 Requires:       ocaml-zip-devel%{?_isa}
 
 %description -n ocaml-%{name}-devel
-This package contains development files needed to build applications
-that use the ocaml-%{name} library.
+This package contains development files needed to build applications that use
+the ocaml-%{name} library.
 
 %package proofgeneral
 Summary:        Why3 integration with ProofGeneral
@@ -161,13 +149,9 @@ sed -e 's|-Wall|%{build_cflags} %{build_ldflags}|;s/ -O -g//' \
 sed -i.orig 's,(MY_PATH_TO_WHY3)/share/whyitp,%{_emacs_sitelispdir},' share/whyitp/README
 fixtimestamp share/whyitp/README
 
-# Fix a configure script typo
-sed -i 's/\$(OCAMLC/$(ocamlc/' configure
-
 %build
 %configure --enable-verbose-make --enable-bddinfer
-# Work around a Makefile bug in version 1.8.0
-ln -s why3.opt bin/why3
+
 # FIXME: Parallel make sometimes fails
 make
 # The documentation build is broken in the 1.8.0 release
@@ -196,8 +180,8 @@ mkdir -p %{buildroot}%{zsh_completions_dir}
 cp -p share/zsh/_why3 %{buildroot}%{zsh_completions_dir}
 
 # Install the LaTeX style
-mkdir -p %{buildroot}%{_texmf}/tex/latex/why3
-cp -p share/latex/why3lang.sty %{buildroot}%{_texmf}/tex/latex/why3
+mkdir -p %{buildroot}%{_texmf_main}/tex/latex/why3
+cp -p share/latex/why3lang.sty %{buildroot}%{_texmf_main}/tex/latex/why3
 
 # Move the gtksourceview language file to the right place
 mkdir -p %{buildroot}%{_datadir}/gtksourceview-3.0
@@ -220,10 +204,10 @@ appstream-util validate-relax --nonet \
   %{buildroot}%{_metainfodir}/fr.lri.%{name}.metainfo.xml
 
 # Move the vim file to the right place
-mkdir -p %{buildroot}%{_datadir}/vim/vimfiles
+mkdir -p %{buildroot}%{vimfiles_root}
 mv %{buildroot}%{_datadir}/%{name}/vim/ftdetect \
    %{buildroot}%{_datadir}/%{name}/vim/syntax \
-   %{buildroot}%{_datadir}/vim/vimfiles
+   %{buildroot}%{vimfiles_root}
 
 # Byte compile the Emacs support files
 cp -p share/whyitp/whyitp.el %{buildroot}%{_emacs_sitelispdir}
@@ -254,9 +238,9 @@ chmod 0755 %{buildroot}%{_bindir}/* \
 %{_datadir}/gtksourceview-3.0/language-specs/%{name}c.lang
 %{_datadir}/gtksourceview-3.0/language-specs/%{name}py.lang
 %{_datadir}/icons/hicolor/scalable/apps/%{name}.svg
-%{_datadir}/vim/vimfiles/ftdetect/%{name}.vim
-%{_datadir}/vim/vimfiles/syntax/%{name}.vim
-%{_texmf}/tex/latex/why3/
+%{vimfiles_root}/ftdetect/%{name}.vim
+%{vimfiles_root}/syntax/%{name}.vim
+%{_texmf_main}/tex/latex/why3/
 %{_libdir}/%{name}/
 %{_metainfodir}/fr.lri.%{name}.metainfo.xml