Hello community,
here is the log from the commit of package coq for openSUSE:Factory checked in
at 2020-08-06 10:42:44
++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
Comparing /work/SRC/openSUSE:Factory/coq (Old)
and /work/SRC/openSUSE:Factory/.coq.new.3399 (New)
++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
Package is "coq"
Thu Aug 6 10:42:44 2020 rev:6 rq:824553 version:8.12.0
Changes:
--------
--- /work/SRC/openSUSE:Factory/coq/coq.changes 2020-06-07 21:38:17.661445539
+0200
+++ /work/SRC/openSUSE:Factory/.coq.new.3399/coq.changes 2020-08-06
10:43:00.054146505 +0200
@@ -1,0 +2,25 @@
+Tue Jul 28 21:48:40 UTC 2020 - Aaron Puchert <aaronpuch...@alice-dsl.net>
+
+- Update to version 8.12.0.
+ * New binder notation for non-maximal implicit arguments using []
+ allowing to set and see the implicit status of arguments
+ immediately.
+ * New notation Inductive "I A | x : s := ..." to distinguish the
+ uniform from the non-uniform parameters in inductive
+ definitions.
+ * More robust and expressive treatment of implicit inductive
+ parameters in inductive declarations.
+ * Improvements in the treatment of implicit arguments and
+ partially applied constants in notations, parsing of
+ hexadecimal number notation and better handling of scopes and
+ coercions for printing.
+ * A correct and efficient coercion coherence checking algorithm,
+ avoiding spurious or duplicate warnings.
+ * An improved Search command which accepts complex queries. This
+ takes precedence over the now deprecated ssreflect search.
+ * Many additions and improvements of the standard library.
+ * Improvements to the reference manual include a more logical
+ organization of chapters along with updated syntax descriptions
+ that match Coq's grammar in most but not all chapters.
+
+-------------------------------------------------------------------
Old:
----
coq-8.11.2.tar.gz
New:
----
coq-8.12.0.tar.gz
++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
Other differences:
------------------
++++++ coq.spec ++++++
--- /var/tmp/diff_new_pack.EbV0bY/_old 2020-08-06 10:43:03.098148030 +0200
+++ /var/tmp/diff_new_pack.EbV0bY/_new 2020-08-06 10:43:03.102148032 +0200
@@ -18,7 +18,7 @@
Name: coq
-Version: 8.11.2
+Version: 8.12.0
Release: 0
Summary: Proof Assistant based on the Calculus of Inductive
Constructions
License: LGPL-2.1-only
@@ -169,6 +169,7 @@
%{_bindir}/coqtop.opt
%{_bindir}/coqwc
%{_bindir}/coqworkmgr
+%{_bindir}/ocamllibdep
%{_bindir}/votour
%dir %{_libdir}/coq
++++++ coq-8.11.2.tar.gz -> coq-8.12.0.tar.gz ++++++
/work/SRC/openSUSE:Factory/coq/coq-8.11.2.tar.gz
/work/SRC/openSUSE:Factory/.coq.new.3399/coq-8.12.0.tar.gz differ: char 13,
line 1
