diff --git a/why3.spec b/why3.spec
index 93984b7..086719a 100644
--- a/why3.spec
+++ b/why3.spec
@@ -9,7 +9,7 @@
 
 Name:           why3
 Version:        1.3.1
-Release:        2%{?dist}
+Release:        6%{?dist}
 Summary:        Software verification platform
 
 # See LICENSE for the terms of the exception
@@ -35,7 +35,6 @@ BuildRequires:  ocaml-findlib
 BuildRequires:  ocaml-lablgtk3-sourceview3-devel
 BuildRequires:  ocaml-ocamldoc
 BuildRequires:  ocaml-menhir-devel
-BuildRequires:  ocaml-mlmpfr-devel
 BuildRequires:  ocaml-num-devel
 BuildRequires:  ocaml-zarith-devel
 BuildRequires:  ocaml-zip-devel
@@ -53,15 +52,26 @@ BuildRequires:  tex(wrapfig.sty)
 BuildRequires:  tex-urlbst
 BuildRequires:  emacs xemacs xemacs-packages-extra
 
-Requires:       gtksourceview3
+Requires:       gtksourceview3%{?_isa}
 Requires:       hicolor-icon-theme
-Requires:       texlive-base
+Requires:       texlive-base%{?_isa}
 Requires:       vim-filesystem
+
+Recommends:     bash-completion
+
 Provides:       bundled(jquery)
 
 # The corresponding Provides is not generated, so filter this out
 %global __requires_exclude ocaml\\\(Why3\\\)
 
+# This can be removed when F36 reaches EOL
+Obsoletes:      why < 2.41-12
+Provides:       why = 2.41-12%{?dist}
+Obsoletes:      why-jessie < 2.41-12
+Provides:       why-jessie = 2.41-12%{?dist}
+Obsoletes:      why-pvs-support < 2.41-12
+Provides:       why-pvs-support = 2.41-12%{?dist}
+
 %description
 Why3 is the next generation of the Why software verification platform.
 Why3 clearly separates the purely logical specification part from
@@ -99,7 +109,11 @@ This package contains an XEmacs support file for working with %{name} files.
 %package all
 Summary:        Complete Why3 software verification platform suite
 Requires:       %{name}%{?_isa} = %{version}-%{release}
-Requires:       alt-ergo coq cvc4 E yices-tools z3 zenon
+Requires:       alt-ergo coq cvc4 E gappa yices-tools z3 zenon
+
+# This can be removed when F36 reaches EOL
+Obsoletes:      why-all < 2.41-12
+Provides:       why-all = 2.41-12%{?dist}
 
 %description all
 This package provides a complete software verification platform suite
@@ -107,6 +121,8 @@ based on Why3, including various automated and interactive provers.
 
 %package -n ocaml-%{name}
 Summary:        Software verification library for ocaml
+Requires:       ocaml-num%{?_isa}
+Requires:       ocaml-zip-devel%{?_isa}
 
 %description -n ocaml-%{name}
 This package contains an ocaml library that exposes the functionality
@@ -119,7 +135,6 @@ Requires:       ocaml-menhir%{?_isa}
 Requires:       ocaml-num-devel%{?_isa}
 Requires:       ocaml-re-devel%{?_isa}
 Requires:       ocaml-seq-devel%{?_isa}
-Requires:       ocaml-zip-devel%{?_isa}
 
 %description -n ocaml-%{name}-devel
 This package contains development files needed to build applications
@@ -144,11 +159,14 @@ fixtimestamp() {
 }
 
 # Use the correct compiler flags, keep timestamps, and harden the build due to
-# network use
+# network use.  Force native compilation when available.
 # Link the binaries with runtime compiled with -fPIC.
 # This avoids many link-time errors.
 sed -e "s|-Wall|$RPM_OPT_FLAGS|;s/ -O -g//" \
     -e "s/cp /cp -p /" \
+%ifarch %{ocaml_native_compiler}
+    -e 's/\$(COQC)/& -native-compiler yes/' \
+%endif
     -e "s|^OLINKFLAGS =.*|& -runtime-variant _pic -ccopt \"$RPM_LD_FLAGS\"|" \
     -i Makefile.in
 
@@ -169,10 +187,6 @@ fixtimestamp examples/bts/20881.why
 sed -i.orig 's,(MY_PATH_TO_WHY3)/share/whyitp,%{_emacs_sitelispdir},' share/whyitp/README
 fixtimestamp share/whyitp/README
 
-# Fix building with mlmpfr support
-sed -i '/EXTPKGS/s/@ZIPLIB@/& @MLMPFR@/' Makefile.in
-sed -i 's/4\.0\.0/4.0.2/g' configure
-
 %build
 %configure --enable-verbose-make
 make #%%{?_smp_mflags}
@@ -183,6 +197,15 @@ rm -f doc/html/.buildinfo examples/use_api/.merlin.in
 make install DESTDIR=%{buildroot}
 make install-lib DESTDIR=%{buildroot}
 
+%ifarch %{ocaml_native_compiler}
+# Install the native coq files
+cd lib/coq
+for dir in $(find . -name .coq-native); do
+  cp -a $dir %{buildroot}%{_libdir}/%{name}/coq/$dir
+done
+cd -
+%endif
+
 # Install the man pages
 mkdir -p %{buildroot}%{_mandir}/man1
 cd man
@@ -255,7 +278,7 @@ chmod 0755 %{buildroot}%{_bindir}/* \
 %{_bindir}/%{name}
 %{_datadir}/%{name}/
 %{_datadir}/applications/%{name}.desktop
-%{_datadir}/bash-completion/
+%{_datadir}/bash-completion/completions/why3
 %{_datadir}/gtksourceview-3.0/language-specs/%{name}.lang
 %{_datadir}/gtksourceview-3.0/language-specs/%{name}c.lang
 %{_datadir}/gtksourceview-3.0/language-specs/%{name}py.lang
@@ -303,6 +326,22 @@ chmod 0755 %{buildroot}%{_bindir}/* \
 %files all
 
 %changelog
+* Mon Jun 15 2020 Jerry James <loganjerry@gmail.com> - 1.3.1-6
+- Rebuild for coq 8.11.2
+- Build the coq files with the native compiler when possible
+
+* Wed May 20 2020 Jerry James <loganjerry@gmail.com> - 1.3.1-5
+- Rebuild for coq 8.11.1
+
+* Sun Apr 12 2020 Jerry James <loganjerry@gmail.com> - 1.3.1-4
+- Make the dependencies on ocaml-num and ocaml-zip explicit (bz 1795083)
+
+* Wed Apr  8 2020 Jerry James <loganjerry@gmail.com> - 1.3.1-3
+- Rebuild for flocq 3.2.1
+- Do not build with mlmpfr; symbols clash with mlgmpidl, causing frama-c to
+  fail to start
+- Obsolete the why2 packages
+
 * Sat Mar 28 2020 Jerry James <loganjerry@gmail.com> - 1.3.1-2
 - Remove useless BRs and Rs (bz 1817878)