rpm/coq
SHA256
1
0
Fork 0
forked from pool/coq
Code Pull Requests Activity

Accepting request 824553 from science

Browse Source 
- 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.

OBS-URL: https://build.opensuse.org/request/show/824553
OBS-URL: https://build.opensuse.org/package/show/openSUSE:Factory/coq?expand=0&rev=6
This commit is contained in:
Dominique Leuenberger 2020-08-06 08:42:44 +00:00 committed by Git OBS Bridge
commit da3c57af9f
4 changed files with 30 additions and 4 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

3
coq-8.11.2.tar.gz
View File

@ -1,3 +0,0 @@
version https://git-lfs.github.com/spec/v1
oid sha256:98cb9e12ba2508a1ca59e0c638fce27bf95c37082b6f7ce355779b80b25e1bfd
size 6564523

3
coq-8.12.0.tar.gz Normal file
View File

@ -0,0 +1,3 @@
version https://git-lfs.github.com/spec/v1
oid sha256:ecde14c6132f5abb459e7f4724788788928174ad4484fff88e86b0086779bcee
size 6774001

25
coq.changes
View File

@ -1,3 +1,28 @@
-------------------------------------------------------------------
Tue Jul 28 21:48:40 UTC 2020 - Aaron Puchert <aaronpuchert@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.
-------------------------------------------------------------------
Sat Jun 6 12:11:06 UTC 2020 - Aaron Puchert <aaronpuchert@alice-dsl.net>

3
coq.spec
View File

@ -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 @@ find %{buildroot}%{_libdir}/coq -name '*.a' \
%{_bindir}/coqtop.opt
%{_bindir}/coqwc
%{_bindir}/coqworkmgr
%{_bindir}/ocamllibdep
%{_bindir}/votour
%dir %{_libdir}/coq