diff --git a/README.md b/README.md new file mode 100644 index 0000000..92f51c8 --- /dev/null +++ b/README.md @@ -0,0 +1,9 @@ +# 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. diff --git a/sources b/sources index 1567f91..bf4128f 100644 --- a/sources +++ b/sources @@ -1,2 +1,2 @@ -SHA512 (zenon-0.8.4.tar.gz) = a60ad321e7eedc00390d11ff91f25d64c7a3fe2eafa23a330e345df02a30ca6964a40e4495b7eeb25e19ed9b7f61b65772c3184ff2b2f85b03e63dc481645e91 +SHA512 (zenon-0.8.5.tar.gz) = dc97cc02bcc2e76a1130f4f7e44ba9839126b5e15f4488ac32d47aef330cbb9ea8c2f1b34f8543ed243587e95848a7187c003a300feed0da64ec81f4501b3bdb SHA512 (zenlpar07.pdf) = f8a24ba1c32015ea315946042b39f0b629094553097f43c8fb37041450d39b64e3a781006bdcbae42919104907efec9f0cf065d675f3ff09af891d9d28c2549f diff --git a/zenon-coq89.patch b/zenon-coq89.patch deleted file mode 100644 index 9e28577..0000000 --- a/zenon-coq89.patch +++ /dev/null @@ -1,174 +0,0 @@ ---- 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]. diff --git a/zenon-deprecated.patch b/zenon-deprecated.patch new file mode 100644 index 0000000..a4bf9fa --- /dev/null +++ b/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). diff --git a/zenon-ocaml.patch b/zenon-ocaml.patch deleted file mode 100644 index c03e325..0000000 --- a/zenon-ocaml.patch +++ /dev/null @@ -1,55 +0,0 @@ ---- 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 diff --git a/zenon.rpmlintrc b/zenon.rpmlintrc deleted file mode 100644 index cd62189..0000000 --- a/zenon.rpmlintrc +++ /dev/null @@ -1,8 +0,0 @@ -# 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') diff --git a/zenon.spec b/zenon.spec index 2a627bf..b208d71 100644 --- a/zenon.spec +++ b/zenon.spec @@ -1,47 +1,46 @@ -%ifnarch %{ocaml_native_compiler} %global debug_package %{nil} -%endif -%global coqver 8.13.0 +%global rocqver 9.2.0 +%global giturl https://github.com/zenon-prover/zenon Name: zenon -Version: 0.8.4 -Release: 21%{?dist} +Version: 0.8.5 +Release: 43%{?dist} Summary: Automated theorem prover for first-order classical logic -License: BSD +License: BSD-3-Clause URL: http://zenon-prover.org/ -Source0: https://github.com/zenon-prover/%{name}/archive/%{version}/%{name}-%{version}.tar.gz +VCS: git:%{giturl}.git +Source0: %{giturl}/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 -# Adapt to coq 8.9 -Patch0: %{name}-coq89.patch -# Adapt to ocaml 4.08 and later -Patch1: %{name}-ocaml.patch +# Update deprecated usage +Patch: %{name}-deprecated.patch -# https://bugzilla.redhat.com/show_bug.cgi?id=1874879 -ExcludeArch: s390x +# Rocq's plugin architecture requires cmxs files +ExclusiveArch: %{ocaml_native_compiler} -BuildRequires: coq = %{coqver} -BuildRequires: ghostscript-core -BuildRequires: ImageMagick +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 -p0 +%autosetup -p1 cp -p %{SOURCE1} . @@ -55,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 @@ -95,10 +88,162 @@ fi %license LICENSE %{_bindir}/%{name} %{_libdir}/coq/user-contrib/Zenon -%{_mandir}/man1/* -%{_mandir}/man5/* +%{_mandir}/man1/zenon.1* +%{_mandir}/man5/zenon-format.5* %changelog +* Wed Jul 29 2026 Jerry James - 0.8.5-43 +- Rebuild to fix rocq dependencies + +* Fri Jul 17 2026 Fedora Release Engineering - 0.8.5-42 +- Rebuilt for https://fedoraproject.org/wiki/Fedora_45_Mass_Rebuild + +* Thu Jul 09 2026 Jerry James - 0.8.5-41 +- OCaml 5.5.0 rebuild + +* Thu Apr 16 2026 Jerry James - 0.8.5-40 +- Rebuild for rocq 9.2.0 + +* Thu Mar 19 2026 Jerry James - 0.8.5-39 +- Rebuild for rocq 9.1.1 + +* Fri Feb 20 2026 Richard W.M. Jones - 0.8.5-38 +- OCaml 5.4.1 rebuild + +* Sat Jan 17 2026 Fedora Release Engineering - 0.8.5-37 +- Rebuilt for https://fedoraproject.org/wiki/Fedora_44_Mass_Rebuild + +* Tue Oct 14 2025 Richard W.M. Jones - 0.8.5-36 +- OCaml 5.4.0 rebuild + +* Fri Aug 22 2025 Jerry James - 0.8.5-35 +- Bump and rebuild + +* Sun Aug 10 2025 Jerry James - 0.8.5-34 +- Bump and rebuild + +* Fri Jul 25 2025 Fedora Release Engineering - 0.8.5-33 +- Rebuilt for https://fedoraproject.org/wiki/Fedora_43_Mass_Rebuild + +* Sat Jul 12 2025 Jerry James - 0.8.5-32 +- Rebuild to fix OCaml dependencies + +* Wed Jan 22 2025 Jerry James - 0.8.5-31 +- Rebuild for coq 8.20.1 + +* Sun Jan 19 2025 Fedora Release Engineering - 0.8.5-30 +- Rebuilt for https://fedoraproject.org/wiki/Fedora_42_Mass_Rebuild + +* Fri Jan 10 2025 Jerry James - 0.8.5-29 +- OCaml 5.3.0 rebuild for Fedora 42 + +* Sat Jul 20 2024 Fedora Release Engineering - 0.8.5-28 +- Rebuilt for https://fedoraproject.org/wiki/Fedora_41_Mass_Rebuild + +* Wed Jun 19 2024 Richard W.M. Jones - 0.8.5-27 +- OCaml 5.2.0 ppc64le fix + +* Wed May 29 2024 Richard W.M. Jones - 0.8.5-26 +- OCaml 5.2.0 for Fedora 41 + +* Fri Feb 2 2024 Jerry James - 0.8.5-25 +- Rebuild for rebuilt coq + +* Sat Jan 27 2024 Fedora Release Engineering - 0.8.5-24 +- Rebuilt for https://fedoraproject.org/wiki/Fedora_40_Mass_Rebuild + +* Tue Jan 2 2024 Jerry James - 0.8.5-23 +- Rebuild for coq 8.18.0 + +* Mon Dec 18 2023 Richard W.M. Jones - 0.8.5-22 +- OCaml 5.1.1 + s390x code gen fix for Fedora 40 + +* Tue Dec 12 2023 Richard W.M. Jones - 0.8.5-21 +- OCaml 5.1.1 rebuild for Fedora 40 + +* Thu Oct 05 2023 Richard W.M. Jones - 0.8.5-20 +- OCaml 5.1 rebuild for Fedora 40 + +* Thu Jul 27 2023 Jerry James - 0.8.5-19 +- Rebuild for ocaml-zarith 1.13 + +* Sat Jul 22 2023 Fedora Release Engineering - 0.8.5-18 +- Rebuilt for https://fedoraproject.org/wiki/Fedora_39_Mass_Rebuild + +* Wed Jul 12 2023 Richard W.M. Jones - 0.8.5-17 +- OCaml 5.0 rebuild for Fedora 39 + +* Mon Jul 10 2023 Jerry James - 0.8.5-16 +- OCaml 5.0.0 rebuild + +* Sat Apr 1 2023 Jerry James - 0.8.5-15 +- Rebuild for coq 8.17.0 + +* Tue Jan 24 2023 Richard W.M. Jones - 0.8.5-14 +- Bump release and rebuild + +* Tue Jan 24 2023 Richard W.M. Jones - 0.8.5-13 +- Rebuild OCaml packages for F38 + +* Sat Jan 21 2023 Fedora Release Engineering - 0.8.5-12 +- Rebuilt for https://fedoraproject.org/wiki/Fedora_38_Mass_Rebuild + +* Sat Nov 26 2022 Jerry James - 0.8.5-11 +- Rebuild for coq 8.16.1 + +* Fri Sep 16 2022 Jerry James - 0.8.5-10 +- Rebuild for coq 8.16.0 + +* Thu Aug 18 2022 Jerry James - 0.8.5-9 +- Rebuild to fix coq dependency +- Convert License tag to SPDX + +* Sat Jul 23 2022 Fedora Release Engineering - 0.8.5-8 +- Rebuilt for https://fedoraproject.org/wiki/Fedora_37_Mass_Rebuild + +* Wed Jul 20 2022 Jerry James - 0.8.5-7 +- Remove i686 support + +* Sun Jun 19 2022 Richard W.M. Jones - 0.8.5-7 +- OCaml 4.14.0 rebuild + +* Fri Mar 25 2022 Jerry James - 0.8.5-6 +- Rebuild for coq 8.15.1 + +* Mon Feb 28 2022 Jerry James - 0.8.5-5 +- Rebuild for coq 8.15.0 + +* Fri Feb 04 2022 Richard W.M. Jones - 0.8.5-4 +- OCaml 4.13.1 rebuild to remove package notes + +* Sat Jan 22 2022 Fedora Release Engineering - 0.8.5-3 +- Rebuilt for https://fedoraproject.org/wiki/Fedora_36_Mass_Rebuild + +* Tue Nov 30 2021 Jerry James - 0.8.5-2 +- Rebuild for coq 8.14.1 + +* Thu Oct 21 2021 Jerry James - 0.8.5-1 +- Version 0.8.5 +- Drop upstreamed -coq89 and -ocaml patches + +* Tue Oct 05 2021 Richard W.M. Jones - 0.8.4-27 +- OCaml 4.13.1 build + +* Mon Oct 04 2021 Richard W.M. Jones - 0.8.4-26 +- Try to build on s390x with OCaml 4.13 + +* Fri Jul 23 2021 Fedora Release Engineering - 0.8.4-25 +- Rebuilt for https://fedoraproject.org/wiki/Fedora_35_Mass_Rebuild + +* Tue Jun 8 2021 Jerry James - 0.8.4-24 +- Rebuild for coq 8.13.2 + +* Wed Mar 3 2021 Jerry James - 0.8.4-23 +- Rebuild for coq 8.13.1 + +* Tue Mar 2 11:03:37 GMT 2021 Richard W.M. Jones - 0.8.4-22 +- OCaml 4.12.0 build + * Sat Feb 20 2021 Jerry James - 0.8.4-21 - Rebuild for coq 8.13.0