Rebuild to fix rocq dependencies

- Add patch to avoid deprecated usage

zenon-deprecated.patch

@@ -0,0 +1,34 @@
+--- zenon-0.8.5/zenon_coqbool.v.orig	2020-10-23 09:19:07.000000000 -0600
++++ zenon-0.8.5/zenon_coqbool.v	2026-03-03 16:33:33.636474063 -0700
+@@ -1,6 +1,6 @@
+ (*  Copyright 2004 INRIA  *)
+ 
+-Require Export Bool.
++From Stdlib Require Export Bool.
+ 
+ Definition __g_not_b := negb.
+ Definition __g_and_b := andb.
+--- zenon-0.8.5/zenon_focal.v.orig	2020-10-23 09:19:07.000000000 -0600
++++ zenon-0.8.5/zenon_focal.v	2026-03-03 16:34:30.531982864 -0700
+@@ -1,8 +1,8 @@
+ (*  Copyright 2004 INRIA  *)
+ 
+-Require Export Bool.
+-Require Import ClassicalEpsilon.
+-Require List.
++From Stdlib Require Export Bool.
++From Stdlib Require Import ClassicalEpsilon.
++From Stdlib Require List.
+ 
+ (* magic: this whole file depends on the following definitions:
+    basics.and_b := andb
+--- zenon-0.8.5/zenon.v.orig	2020-10-23 09:19:07.000000000 -0600
++++ zenon-0.8.5/zenon.v	2026-03-03 16:33:06.988515450 -0700
+@@ -1,6 +1,6 @@
+ (*  Copyright 2004 INRIA  *)
+ 
+-Require Export Classical.
++From Stdlib Require Export Classical.
+ 
+ Lemma zenon_notnot : forall P : Prop,
+   P -> (~ P -> False).

zenon.spec

@@ -1,15 +1,10 @@
-# Coq's plugin architecture requires cmxs files, so:
-ExclusiveArch: %{ocaml_native_compiler}
-
-%ifnarch %{ocaml_native_compiler}
 %global debug_package %{nil}
-%endif
-%global coqver  8.18.0
+%global rocqver 9.2.0
 %global giturl  https://github.com/zenon-prover/zenon
 
 Name:		zenon
 Version:	0.8.5
-Release:	28%{?dist}
+Release:	43%{?dist}
 Summary:	Automated theorem prover for first-order classical logic
 License:	BSD-3-Clause
 URL:		http://zenon-prover.org/
@@ -21,25 +16,31 @@ Source3:	%{name}-tptp-ReadMe
 # Basic documentation (man pages). Submitted upstream 2008-07-25:
 Source4:	%{name}.1
 Source5:	%{name}-format.5
+# Update deprecated usage
+Patch:          %{name}-deprecated.patch
 
-BuildRequires:	coq = %{coqver}
-BuildRequires:	ghostscript
-BuildRequires:	ImageMagick
+# Rocq's plugin architecture requires cmxs files
+ExclusiveArch:  %{ocaml_native_compiler}
+
+BuildRequires:	coq-core-compat = %{rocqver}
+BuildRequires:	rocq = %{rocqver}
+BuildRequires:	rocq-stdlib
 BuildRequires:	make
 BuildRequires:	ocaml
 
-Requires:	coq%{?_isa} = %{coqver}
+Requires:	rocq%{?_isa} = %{rocqver}
+Requires:	rocq-stdlib%{?_isa}
 Requires:	coreutils
 
 %description
-Zenon is an automated theorem prover for first order classical logic
-with equality, based on the tableau method.  Zenon can read input files
-in TPTP, Coq, Focal, and its own Zenon format.  Zenon can directly
-generate Coq proofs (proof scripts or proof terms), which can be
-reinserted into Coq specifications.  Zenon can also be extended.
+Zenon is an automated theorem prover for first order classical logic with
+equality, based on the tableau method.  Zenon can read input files in TPTP,
+Coq, Focal, and its own Zenon format.  Zenon can directly generate Coq proofs
+(proof scripts or proof terms), which can be reinserted into Coq
+specifications.  Zenon can also be extended.
 
 %prep
-%autosetup
+%autosetup -p1
 
 cp -p %{SOURCE1} .
 
@@ -53,14 +54,8 @@ mkdir examples
 cp -p %{SOURCE2} examples/tptp-COM003+2.p
 cp -p %{SOURCE3} examples/tptp-ReadMe
 
-# Work around Makefile errors (fails if no ocamlopt, uses _bytecode_ otherwise)
-%ifarch %{ocaml_native_compiler}
-  make %{?_smp_mflags} zenon.bin
-  cp -p zenon.bin zenon
-%else
-  make %{?_smp_mflags} zenon.byt
-  cp -p zenon.byt zenon
-%endif
+make %{?_smp_mflags} zenon.bin
+cp -p zenon.bin zenon
 # Use of %%{?_smp_mflags} sometimes leads to build failures
 make coq
 
@@ -97,6 +92,51 @@ fi
 %{_mandir}/man5/zenon-format.5*
 
 %changelog
+* Wed Jul 29 2026 Jerry James <loganjerry@gmail.com> - 0.8.5-43
+- Rebuild to fix rocq dependencies
+
+* Fri Jul 17 2026 Fedora Release Engineering <releng@fedoraproject.org> - 0.8.5-42
+- Rebuilt for https://fedoraproject.org/wiki/Fedora_45_Mass_Rebuild
+
+* Thu Jul 09 2026 Jerry James <loganjerry@gmail.com> - 0.8.5-41
+- OCaml 5.5.0 rebuild
+
+* Thu Apr 16 2026 Jerry James <loganjerry@gmail.com> - 0.8.5-40
+- Rebuild for rocq 9.2.0
+
+* Thu Mar 19 2026 Jerry James <loganjerry@gmail.com> - 0.8.5-39
+- Rebuild for rocq 9.1.1
+
+* Fri Feb 20 2026 Richard W.M. Jones <rjones@redhat.com> - 0.8.5-38
+- OCaml 5.4.1 rebuild
+
+* Sat Jan 17 2026 Fedora Release Engineering <releng@fedoraproject.org> - 0.8.5-37
+- Rebuilt for https://fedoraproject.org/wiki/Fedora_44_Mass_Rebuild
+
+* Tue Oct 14 2025 Richard W.M. Jones <rjones@redhat.com> - 0.8.5-36
+- OCaml 5.4.0 rebuild
+
+* Fri Aug 22 2025 Jerry James <loganjerry@gmail.com> - 0.8.5-35
+- Bump and rebuild
+
+* Sun Aug 10 2025 Jerry James <loganjerry@gmail.com> - 0.8.5-34
+- Bump and rebuild
+
+* Fri Jul 25 2025 Fedora Release Engineering <releng@fedoraproject.org> - 0.8.5-33
+- Rebuilt for https://fedoraproject.org/wiki/Fedora_43_Mass_Rebuild
+
+* Sat Jul 12 2025 Jerry James <loganjerry@gmail.com> - 0.8.5-32
+- Rebuild to fix OCaml dependencies
+
+* Wed Jan 22 2025 Jerry James <loganjerry@gmail.com> - 0.8.5-31
+- Rebuild for coq 8.20.1
+
+* Sun Jan 19 2025 Fedora Release Engineering <releng@fedoraproject.org> - 0.8.5-30
+- Rebuilt for https://fedoraproject.org/wiki/Fedora_42_Mass_Rebuild
+
+* Fri Jan 10 2025 Jerry James <loganjerry@gmail.com> - 0.8.5-29
+- OCaml 5.3.0 rebuild for Fedora 42
+
 * Sat Jul 20 2024 Fedora Release Engineering <releng@fedoraproject.org> - 0.8.5-28
 - Rebuilt for https://fedoraproject.org/wiki/Fedora_41_Mass_Rebuild