diff --git a/why3-rocq-9.2.patch b/why3-rocq-9.2.patch
deleted file mode 100644
index 9b2042c..0000000
--- a/why3-rocq-9.2.patch
+++ /dev/null
@@ -1,292 +0,0 @@
---- 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
deleted file mode 100644
index 48f3ae4..0000000
--- a/why3-zmod.patch
+++ /dev/null
@@ -1,33 +0,0 @@
---- 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 3fc4249..7174465 100644
--- a/why3.spec
+++ b/why3.spec
@@ -1,3 +1,6 @@
+# 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
@@ -16,18 +19,12 @@ 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
-# 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
 
-# Coq's plugin architecture requires cmxs files, so:
-ExclusiveArch:  %{ocaml_native_compiler}
-
-BuildRequires:  coq-core-compat
+BuildRequires:  coq
 BuildRequires:  emacs-nw
 BuildRequires:  emacs-proofgeneral
 BuildRequires:  flocq
+BuildRequires:  graphviz
 BuildRequires:  java-devel
 BuildRequires:  latexmk
 BuildRequires:  libappstream-glib
@@ -40,6 +37,7 @@ 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
@@ -47,8 +45,19 @@ BuildRequires:  ocaml-re-devel
 BuildRequires:  ocaml-sexplib-devel
 BuildRequires:  ocaml-zarith-devel
 BuildRequires:  ocaml-zip-devel
-BuildRequires:  rocq
-BuildRequires:  texlive-latex
+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:  vim-filesystem
 
 Requires:       gtksourceview3%{?_isa}
@@ -65,12 +74,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
@@ -95,16 +104,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
@@ -116,8 +125,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