Rebuild for coq 8.13.2.

README.md

@@ -1,9 +0,0 @@
-# zenon
-
-Zenon is an extensible authomated theorem prover whose main claim to fame is
-that it produces actual proofs of theorems.  Correctness is an explicit
-non-goal in the design of Zenon: the proof output needs to be checked by
-another program before the theorem is considered proved.  As a consequence,
-Zenon is not designed for direct use by humans, but rather for interfacing
-into formal proof systems, such as interactive proof assistants and
-non-interactive proof checkers.

sources

@@ -1,2 +1,2 @@
-SHA512 (zenon-0.8.5.tar.gz) = dc97cc02bcc2e76a1130f4f7e44ba9839126b5e15f4488ac32d47aef330cbb9ea8c2f1b34f8543ed243587e95848a7187c003a300feed0da64ec81f4501b3bdb
+SHA512 (zenon-0.8.4.tar.gz) = a60ad321e7eedc00390d11ff91f25d64c7a3fe2eafa23a330e345df02a30ca6964a40e4495b7eeb25e19ed9b7f61b65772c3184ff2b2f85b03e63dc481645e91
 SHA512 (zenlpar07.pdf) = f8a24ba1c32015ea315946042b39f0b629094553097f43c8fb37041450d39b64e3a781006bdcbae42919104907efec9f0cf065d675f3ff09af891d9d28c2549f

zenon-coq89.patch

@@ -0,0 +1,174 @@
+--- zenon_coqbool.v.orig	2018-09-18 09:01:37.000000000 -0600
++++ zenon_coqbool.v	2019-05-31 09:34:36.433667055 -0600
+@@ -143,7 +143,7 @@ Proof.
+   intros A B r cond; unfold Is_true; destruct cond; auto.
+ Qed.
+ 
+-Implicit Arguments zenon_coqbool_ite_rel_l [A B].
++Arguments zenon_coqbool_ite_rel_l [A B].
+ 
+ Lemma zenon_coqbool_ite_rel_r :
+   forall (A B : Type) (r: A -> B -> Prop) (e1 : A) (cond : bool) (thn els : B),
+@@ -154,7 +154,7 @@ Proof.
+   intros A B r e1 cond; unfold Is_true; destruct cond; auto.
+ Qed.
+ 
+-Implicit Arguments zenon_coqbool_ite_rel_r [A B].
++Arguments zenon_coqbool_ite_rel_r [A B].
+ 
+ Lemma zenon_coqbool_ite_rel_nl :
+   forall (A B : Type) (r: A -> B -> Prop) (cond : bool) (thn els : A) (e2 : B),
+@@ -165,7 +165,7 @@ Proof.
+   intros A B r cond; unfold Is_true; destruct cond; auto.
+ Qed.
+ 
+-Implicit Arguments zenon_coqbool_ite_rel_nl [A B].
++Arguments zenon_coqbool_ite_rel_nl [A B].
+ 
+ Lemma zenon_coqbool_ite_rel_nr :
+   forall (A B : Type) (r: A -> B -> Prop) (e1 : A) (cond : bool) (thn els : B),
+@@ -176,7 +176,7 @@ Proof.
+   intros A B r e1 cond; unfold Is_true; destruct cond; auto.
+ Qed.
+ 
+-Implicit Arguments zenon_coqbool_ite_rel_nr [A B].
++Arguments zenon_coqbool_ite_rel_nr [A B].
+ 
+ (* ************************************************ *)
+ 
+@@ -216,19 +216,19 @@ Definition zenon_coqbool_ite_rel_l_s :=
+   fun A B r i t e e2 c h1 h2
+   => @zenon_coqbool_ite_rel_l A B r i t e e2 h1 h2 c
+ .
+-Implicit Arguments zenon_coqbool_ite_rel_l_s [A B].
++Arguments zenon_coqbool_ite_rel_l_s [A B].
+ Definition zenon_coqbool_ite_rel_r_s :=
+   fun A B r e1 i t e c h1 h2
+   => @zenon_coqbool_ite_rel_r A B r e1 i t e h1 h2 c
+ .
+-Implicit Arguments zenon_coqbool_ite_rel_r_s [A B].
++Arguments zenon_coqbool_ite_rel_r_s [A B].
+ Definition zenon_coqbool_ite_rel_nl_s :=
+   fun A B r i t e e2 c h1 h2
+   => @zenon_coqbool_ite_rel_nl A B r i t e e2 h1 h2 c
+ .
+-Implicit Arguments zenon_coqbool_ite_rel_nl_s [A B].
++Arguments zenon_coqbool_ite_rel_nl_s [A B].
+ Definition zenon_coqbool_ite_rel_nr_s :=
+   fun A B r e1 i t e c h1 h2
+   => @zenon_coqbool_ite_rel_nr A B r e1 i t e h1 h2 c
+ .
+-Implicit Arguments zenon_coqbool_ite_rel_nr_s [A B].
++Arguments zenon_coqbool_ite_rel_nr_s [A B].
+--- zenon_focal.v.orig	2018-09-18 09:01:37.000000000 -0600
++++ zenon_focal.v	2019-05-31 09:34:54.814494601 -0600
+@@ -198,7 +198,7 @@ Proof.
+   intros A B r cond; unfold Is_true; destruct cond; auto.
+ Qed.
+ 
+-Implicit Arguments zenon_focal_ite_rel_l [A B].
++Arguments zenon_focal_ite_rel_l [A B].
+ 
+ Lemma zenon_focal_ite_rel_r :
+   forall (A B : Type) (r: A -> B -> Prop) (e1 : A) (cond : bool) (thn els : B),
+@@ -209,7 +209,7 @@ Proof.
+   intros A B r e1 cond; unfold Is_true; destruct cond; auto.
+ Qed.
+ 
+-Implicit Arguments zenon_focal_ite_rel_r [A B].
++Arguments zenon_focal_ite_rel_r [A B].
+ 
+ Lemma zenon_focal_ite_rel_nl :
+   forall (A B : Type) (r: A -> B -> Prop) (cond : bool) (thn els : A) (e2 : B),
+@@ -220,7 +220,7 @@ Proof.
+   intros A B r cond; unfold Is_true; destruct cond; auto.
+ Qed.
+ 
+-Implicit Arguments zenon_focal_ite_rel_nl [A B].
++Arguments zenon_focal_ite_rel_nl [A B].
+ 
+ Lemma zenon_focal_ite_rel_nr :
+   forall (A B : Type) (r: A -> B -> Prop) (e1 : A) (cond : bool) (thn els : B),
+@@ -231,7 +231,7 @@ Proof.
+   intros A B r e1 cond; unfold Is_true; destruct cond; auto.
+ Qed.
+ 
+-Implicit Arguments zenon_focal_ite_rel_nr [A B].
++Arguments zenon_focal_ite_rel_nr [A B].
+ 
+ Lemma zenon_focal_istrue_true : forall e,
+   (e = true -> False) -> (Is_true e -> False).
+@@ -313,19 +313,19 @@ Definition zenon_focal_ite_rel_l_s :=
+   fun A B r i t e e2 c h1 h2
+   => @zenon_focal_ite_rel_l A B r i t e e2 h1 h2 c
+ .
+-Implicit Arguments zenon_focal_ite_rel_l_s [A B].
++Arguments zenon_focal_ite_rel_l_s [A B].
+ Definition zenon_focal_ite_rel_r_s :=
+   fun A B r e1 i t e c h1 h2
+   => @zenon_focal_ite_rel_r A B r e1 i t e h1 h2 c
+ .
+-Implicit Arguments zenon_focal_ite_rel_r_s [A B].
++Arguments zenon_focal_ite_rel_r_s [A B].
+ Definition zenon_focal_ite_rel_nl_s :=
+   fun A B r i t e e2 c h1 h2
+   => @zenon_focal_ite_rel_nl A B r i t e e2 h1 h2 c
+ .
+-Implicit Arguments zenon_focal_ite_rel_nl_s [A B].
++Arguments zenon_focal_ite_rel_nl_s [A B].
+ Definition zenon_focal_ite_rel_nr_s :=
+   fun A B r e1 i t e c h1 h2
+   => @zenon_focal_ite_rel_nr A B r e1 i t e h1 h2 c
+ .
+-Implicit Arguments zenon_focal_ite_rel_nr_s [A B].
++Arguments zenon_focal_ite_rel_nr_s [A B].
+--- zenon_induct.v.orig	2018-09-18 09:01:37.000000000 -0600
++++ zenon_induct.v	2019-05-31 09:39:07.572218768 -0600
+@@ -12,13 +12,13 @@ Lemma zenon_induct_f_equal : forall (T1
+   (f x = f y -> False) -> (x = y -> False).
+   Proof. intros T1 T2 x y f H1 H2. apply H1. subst x. auto. Qed.
+ 
+-Implicit Arguments zenon_induct_f_equal [T1 T2].
++Arguments zenon_induct_f_equal [T1 T2].
+ 
+ Definition zenon_induct_f_equal_s :=
+   fun t1 t2 x y f c h => @zenon_induct_f_equal t1 t2 x y f h c
+ .
+ 
+-Implicit Arguments zenon_induct_f_equal_s [t1 t2].
++Arguments zenon_induct_f_equal_s [t1 t2].
+ 
+ Lemma zenon_induct_case_subs : forall (T : Type) (b a : T) P,
+   (b = a -> P(a) -> False) -> b = a -> P(b) -> False.
+--- zenon.v.orig	2018-09-18 09:01:37.000000000 -0600
++++ zenon.v	2019-05-31 09:34:15.884859849 -0600
+@@ -71,7 +71,7 @@ Lemma zenon_notallex : forall (T : Type)
+ Proof.
+   firstorder. apply H0. intro x. apply NNPP. intro nPx. apply (H x nPx).
+ Qed.
+-Implicit Arguments zenon_notallex [T].
++Arguments zenon_notallex [T].
+ 
+ Lemma zenon_subst :
+   forall (T : Type) (P : T -> Prop) (a b : T),
+@@ -111,7 +111,7 @@ Definition zenon_notequiv_s := fun P Q c
+ Definition zenon_ex_s := fun T P c h => zenon_ex T P h c.
+ Definition zenon_notall_s := fun T P c h => zenon_notall T P h c.
+ Definition zenon_notallex_s := fun T P c h => @zenon_notallex T P h c.
+-Implicit Arguments zenon_notallex_s [T].
++Arguments zenon_notallex_s [T].
+ 
+ Definition zenon_subst_s := fun T P x y c h i => zenon_subst T P x y h i c.
+ Definition zenon_pnotp_s := fun P Q c h i => zenon_pnotp P Q h i c.
+@@ -142,9 +142,9 @@ Proof.
+   auto.
+ Qed.
+ 
+-Implicit Arguments zenon_recfun_unfold [A].
++Arguments zenon_recfun_unfold [A].
+ 
+ Definition zenon_recfun_unfold_s :=
+   fun A P a b eqn c h => @zenon_recfun_unfold A P a b eqn h c
+ .
+-Implicit Arguments zenon_recfun_unfold_s [A].
++Arguments zenon_recfun_unfold_s [A].

zenon-deprecated.patch

@@ -1,34 +0,0 @@
---- 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-ocaml.patch

@@ -0,0 +1,55 @@
+--- coqterm.ml.orig	2018-09-18 09:01:37.000000000 -0600
++++ coqterm.ml	2020-08-20 13:02:03.239490105 -0600
+@@ -447,7 +447,7 @@ let rec rm_lambdas l term =
+   | _, _ -> assert false
+ ;;
+ 
+-let compare_hyps (name1, _) (name2, _) = Pervasives.compare name1 name2;;
++let compare_hyps (name1, _) (name2, _) = Stdlib.compare name1 name2;;
+ 
+ let make_lemma { name = name; params = params; proof = proof } =
+   let f (ty, e) =
+--- expr.ml.orig	2018-09-18 09:01:37.000000000 -0600
++++ expr.ml	2020-08-20 13:01:38.415478986 -0600
+@@ -364,7 +364,7 @@ let hash = get_hash;;
+ let equal = (==);;
+ let compare x y =
+   match compare (hash x) (hash y) with
+-  | 0 -> if equal x y then 0 else Pervasives.compare x y
++  | 0 -> if equal x y then 0 else Stdlib.compare x y
+   | x when x < 0 -> -1
+   | _ -> 1
+ ;;
+--- ext_induct.ml.orig	2018-09-18 09:01:37.000000000 -0600
++++ ext_induct.ml	2020-08-20 13:03:10.847520391 -0600
+@@ -96,8 +96,8 @@ let rec make_case accu e =
+ 
+ let compare_cases (cs1, _, _) (cs2, _, _) =
+   try
+-    Pervasives.compare (Hashtbl.find constructor_table cs1).cd_num
+-                       (Hashtbl.find constructor_table cs2).cd_num
++    Stdlib.compare (Hashtbl.find constructor_table cs1).cd_num
++                   (Hashtbl.find constructor_table cs2).cd_num
+   with Not_found -> raise Empty
+ ;;
+ 
+--- lltoisar.ml.orig	2018-09-18 09:01:37.000000000 -0600
++++ lltoisar.ml	2020-08-20 13:02:41.168507098 -0600
+@@ -21,7 +21,7 @@ let dict_empty = Dict.empty;;
+ 
+ module Int = struct
+   type t = int;;
+-  let compare = Pervasives.compare;;
++  let compare = Stdlib.compare;;
+ end;;
+ module Hypdict = Map.Make (Int);;
+ 
+@@ -973,7 +973,7 @@ let rec get_nary_rules accu prf =
+ let add_nary_rules oc lemmas =
+   let f lem = get_nary_rules [] lem.proof in
+   let rules = List.flatten (List.map f lemmas) in
+-  let rules1 = Misc.list_sort_unique Pervasives.compare rules in
++  let rules1 = Misc.list_sort_unique Stdlib.compare rules in
+   let f r =
+     match r with
+     | Nary_case (n, oth) -> Isar_case.print_case "have" n oth oc

zenon.rpmlintrc

@@ -0,0 +1,8 @@
+# THIS FILE IS FOR WHITELISTING RPMLINT ERRORS AND WARNINGS IN TASKOTRON
+# https://fedoraproject.org/wiki/Taskotron/Tasks/dist.rpmlint#Whitelisting_errors
+
+# The dictionary is missing some technical terms
+addFilter(r'W: spelling-error .* prover')
+
+# The configure script is not an autotools-generated script
+addFilter(r'zenon\.spec:[^:]*: W: configure-without-libdir-spec')

zenon.spec

@@ -1,46 +1,47 @@
+%ifnarch %{ocaml_native_compiler}
 %global debug_package %{nil}
-%global rocqver 9.2.0
-%global giturl  https://github.com/zenon-prover/zenon
+%endif
+%global coqver 8.13.2
 
 Name:		zenon
-Version:	0.8.5
-Release:	43%{?dist}
+Version:	0.8.4
+Release:	23%{?dist}
 Summary:	Automated theorem prover for first-order classical logic
-License:	BSD-3-Clause
+License:	BSD
 URL:		http://zenon-prover.org/
-VCS:		git:%{giturl}.git
-Source0:	%{giturl}/archive/%{version}/%{name}-%{version}.tar.gz
+Source0:	https://github.com/zenon-prover/%{name}/archive/%{version}/%{name}-%{version}.tar.gz
 Source1:	http://zenon-prover.org/zenlpar07.pdf
 Source2:	%{name}-tptp-COM003+2.p
 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
+# Adapt to coq 8.9
+Patch0:		%{name}-coq89.patch
+# Adapt to ocaml 4.08 and later
+Patch1:		%{name}-ocaml.patch
 
-# Rocq's plugin architecture requires cmxs files
-ExclusiveArch:  %{ocaml_native_compiler}
+# https://bugzilla.redhat.com/show_bug.cgi?id=1874879
+ExcludeArch: s390x
 
-BuildRequires:	coq-core-compat = %{rocqver}
-BuildRequires:	rocq = %{rocqver}
-BuildRequires:	rocq-stdlib
+BuildRequires:	coq = %{coqver}
+BuildRequires:	ghostscript
+BuildRequires:	ImageMagick
 BuildRequires:	make
 BuildRequires:	ocaml
 
-Requires:	rocq%{?_isa} = %{rocqver}
-Requires:	rocq-stdlib%{?_isa}
+Requires:	coq%{?_isa} = %{coqver}
 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 -p1
+%autosetup -p0
 
 cp -p %{SOURCE1} .
 
@@ -54,8 +55,14 @@ mkdir examples
 cp -p %{SOURCE2} examples/tptp-COM003+2.p
 cp -p %{SOURCE3} examples/tptp-ReadMe
 
-make %{?_smp_mflags} zenon.bin
-cp -p zenon.bin zenon
+# 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
 # Use of %%{?_smp_mflags} sometimes leads to build failures
 make coq
 
@@ -88,162 +95,16 @@ fi
 %license LICENSE
 %{_bindir}/%{name}
 %{_libdir}/coq/user-contrib/Zenon
-%{_mandir}/man1/zenon.1*
-%{_mandir}/man5/zenon-format.5*
+%{_mandir}/man1/*
+%{_mandir}/man5/*
 
 %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
-
-* Wed Jun 19 2024 Richard W.M. Jones <rjones@redhat.com> - 0.8.5-27
-- OCaml 5.2.0 ppc64le fix
-
-* Wed May 29 2024 Richard W.M. Jones <rjones@redhat.com> - 0.8.5-26
-- OCaml 5.2.0 for Fedora 41
-
-* Fri Feb  2 2024 Jerry James <loganjerry@gmail.com> - 0.8.5-25
-- Rebuild for rebuilt coq
-
-* Sat Jan 27 2024 Fedora Release Engineering <releng@fedoraproject.org> - 0.8.5-24
-- Rebuilt for https://fedoraproject.org/wiki/Fedora_40_Mass_Rebuild
-
-* Tue Jan  2 2024 Jerry James <loganjerry@gmail.com> - 0.8.5-23
-- Rebuild for coq 8.18.0
-
-* Mon Dec 18 2023 Richard W.M. Jones <rjones@redhat.com> - 0.8.5-22
-- OCaml 5.1.1 + s390x code gen fix for Fedora 40
-
-* Tue Dec 12 2023 Richard W.M. Jones <rjones@redhat.com> - 0.8.5-21
-- OCaml 5.1.1 rebuild for Fedora 40
-
-* Thu Oct 05 2023 Richard W.M. Jones <rjones@redhat.com> - 0.8.5-20
-- OCaml 5.1 rebuild for Fedora 40
-
-* Thu Jul 27 2023 Jerry James <loganjerry@gmail.com> - 0.8.5-19
-- Rebuild for ocaml-zarith 1.13
-
-* Sat Jul 22 2023 Fedora Release Engineering <releng@fedoraproject.org> - 0.8.5-18
-- Rebuilt for https://fedoraproject.org/wiki/Fedora_39_Mass_Rebuild
-
-* Wed Jul 12 2023 Richard W.M. Jones <rjones@redhat.com> - 0.8.5-17
-- OCaml 5.0 rebuild for Fedora 39
-
-* Mon Jul 10 2023 Jerry James <loganjerry@gmail.com> - 0.8.5-16
-- OCaml 5.0.0 rebuild
-
-* Sat Apr  1 2023 Jerry James <loganjerry@gmail.com> - 0.8.5-15
-- Rebuild for coq 8.17.0
-
-* Tue Jan 24 2023 Richard W.M. Jones <rjones@redhat.com> - 0.8.5-14
-- Bump release and rebuild
-
-* Tue Jan 24 2023 Richard W.M. Jones <rjones@redhat.com> - 0.8.5-13
-- Rebuild OCaml packages for F38
-
-* Sat Jan 21 2023 Fedora Release Engineering <releng@fedoraproject.org> - 0.8.5-12
-- Rebuilt for https://fedoraproject.org/wiki/Fedora_38_Mass_Rebuild
-
-* Sat Nov 26 2022 Jerry James <loganjerry@gmail.com> - 0.8.5-11
-- Rebuild for coq 8.16.1
-
-* Fri Sep 16 2022 Jerry James <loganjerry@gmail.com> - 0.8.5-10
-- Rebuild for coq 8.16.0
-
-* Thu Aug 18 2022 Jerry James <loganjerry@gmail.com> - 0.8.5-9
-- Rebuild to fix coq dependency
-- Convert License tag to SPDX
-
-* Sat Jul 23 2022 Fedora Release Engineering <releng@fedoraproject.org> - 0.8.5-8
-- Rebuilt for https://fedoraproject.org/wiki/Fedora_37_Mass_Rebuild
-
-* Wed Jul 20 2022 Jerry James <loganjerry@gmail.com> - 0.8.5-7
-- Remove i686 support
-
-* Sun Jun 19 2022 Richard W.M. Jones <rjones@redhat.com> - 0.8.5-7
-- OCaml 4.14.0 rebuild
-
-* Fri Mar 25 2022 Jerry James <loganjerry@gmail.com> - 0.8.5-6
-- Rebuild for coq 8.15.1
-
-* Mon Feb 28 2022 Jerry James <loganjerry@gmail.com> - 0.8.5-5
-- Rebuild for coq 8.15.0
-
-* Fri Feb 04 2022 Richard W.M. Jones <rjones@redhat.com> - 0.8.5-4
-- OCaml 4.13.1 rebuild to remove package notes
-
-* Sat Jan 22 2022 Fedora Release Engineering <releng@fedoraproject.org> - 0.8.5-3
-- Rebuilt for https://fedoraproject.org/wiki/Fedora_36_Mass_Rebuild
-
-* Tue Nov 30 2021 Jerry James <loganjerry@gmail.com> - 0.8.5-2
-- Rebuild for coq 8.14.1
-
-* Thu Oct 21 2021 Jerry James <loganjerry@gmail.com> - 0.8.5-1
-- Version 0.8.5
-- Drop upstreamed -coq89 and -ocaml patches
-
-* Tue Oct 05 2021 Richard W.M. Jones <rjones@redhat.com> - 0.8.4-27
-- OCaml 4.13.1 build
-
-* Mon Oct 04 2021 Richard W.M. Jones <rjones@redhat.com> - 0.8.4-26
-- Try to build on s390x with OCaml 4.13
-
-* Fri Jul 23 2021 Fedora Release Engineering <releng@fedoraproject.org> - 0.8.4-25
-- Rebuilt for https://fedoraproject.org/wiki/Fedora_35_Mass_Rebuild
-
-* Tue Jun  8 2021 Jerry James <loganjerry@gmail.com> - 0.8.4-24
+* Tue Jun  8 2021 Jerry James <loganjerry@gmail.com> - 0.8.4-23
 - Rebuild for coq 8.13.2
 
-* Wed Mar  3 2021 Jerry James <loganjerry@gmail.com> - 0.8.4-23
+* Wed Mar  3 2021 Jerry James <loganjerry@gmail.com> - 0.8.4-22
 - Rebuild for coq 8.13.1
 
-* Tue Mar  2 11:03:37 GMT 2021 Richard W.M. Jones <rjones@redhat.com> - 0.8.4-22
-- OCaml 4.12.0 build
-
 * Sat Feb 20 2021 Jerry James <loganjerry@gmail.com> - 0.8.4-21
 - Rebuild for coq 8.13.0