From c3225375ef043bf111d9838f10ced14e4e994763665dc8953f17fd63f4651ce3 Mon Sep 17 00:00:00 2001 From: Aaron Puchert Date: Tue, 17 Nov 2020 22:12:19 +0000 Subject: [PATCH] - Update to version 8.12.1. This contains mostly bug fixes: * Polymorphic side-effects inside monomorphic definitions were incorrectly handled as not inlined. This allowed deriving an inconsistency. * Regression in error reporting after SSReflect's case tactic. A generic error message "Could not fill dependent hole in apply" was reported for any error following case or elim. * Several bugs with Search. * The details environment introduced in coqdoc in Coq 8.12 can now be used as advertised in the reference manual. * View menu "Display parentheses" introduced in CoqIDE in Coq 8.12 now works correctly. OBS-URL: https://build.opensuse.org/package/show/science/coq?expand=0&rev=22 --- coq-8.12.0.tar.gz | 3 --- coq-8.12.1.tar.gz | 3 +++ coq.changes | 16 ++++++++++++++++ coq.spec | 2 +- 4 files changed, 20 insertions(+), 4 deletions(-) delete mode 100644 coq-8.12.0.tar.gz create mode 100644 coq-8.12.1.tar.gz diff --git a/coq-8.12.0.tar.gz b/coq-8.12.0.tar.gz deleted file mode 100644 index 8cc8606..0000000 --- a/coq-8.12.0.tar.gz +++ /dev/null @@ -1,3 +0,0 @@ -version https://git-lfs.github.com/spec/v1 -oid sha256:ecde14c6132f5abb459e7f4724788788928174ad4484fff88e86b0086779bcee -size 6774001 diff --git a/coq-8.12.1.tar.gz b/coq-8.12.1.tar.gz new file mode 100644 index 0000000..51b5fbb --- /dev/null +++ b/coq-8.12.1.tar.gz @@ -0,0 +1,3 @@ +version https://git-lfs.github.com/spec/v1 +oid sha256:dabad911239c69ecf79931b513cb427101c2f15f0451af056fbf181df526f8a5 +size 6855317 diff --git a/coq.changes b/coq.changes index 0c10f2a..5fe2c3e 100644 --- a/coq.changes +++ b/coq.changes @@ -1,3 +1,19 @@ +------------------------------------------------------------------- +Tue Nov 17 22:09:12 UTC 2020 - Aaron Puchert + +- Update to version 8.12.1. This contains mostly bug fixes: + * Polymorphic side-effects inside monomorphic definitions were + incorrectly handled as not inlined. This allowed deriving an + inconsistency. + * Regression in error reporting after SSReflect's case tactic. + A generic error message "Could not fill dependent hole in + apply" was reported for any error following case or elim. + * Several bugs with Search. + * The details environment introduced in coqdoc in Coq 8.12 can + now be used as advertised in the reference manual. + * View menu "Display parentheses" introduced in CoqIDE in + Coq 8.12 now works correctly. + ------------------------------------------------------------------- Thu Aug 20 08:33:34 UTC 2020 - Martin Liška diff --git a/coq.spec b/coq.spec index 6c710b6..9a655d4 100644 --- a/coq.spec +++ b/coq.spec @@ -18,7 +18,7 @@ Name: coq -Version: 8.12.0 +Version: 8.12.1 Release: 0 Summary: Proof Assistant based on the Calculus of Inductive Constructions License: LGPL-2.1-only