AU: 1 updated - Coq

[skip ci] https://gist.github.com/747b3ede98c9404e5cb6a399595e7ad1/9752a7787f1cb3cc5df1eb1287eb57782bfa636b

automatic/coq/coq.nuspec

@@ -3,7 +3,7 @@
 <package xmlns="http://schemas.microsoft.com/packaging/2015/06/nuspec.xsd">
   <metadata>
     <id>Coq</id>
-    <version>8.12.1</version>
+    <version>8.13.0</version>
     <packageSourceUrl>https://github.com/admiringworm/chocolatey-packages/tree/master/automatic/coq</packageSourceUrl>
     <owners>AdmiringWorm, murray</owners>
     <title>The Coq proof assistant</title>
@@ -38,17 +38,12 @@ As a platform for the formalization of mathematics or the development of program
 ## [Package Changelog](https://github.com/AdmiringWorm/chocolatey-packages/blob/master/automatic/coq/Changelog.md)
 
 ## Software Release Notes
-This release contains numerous bug fixes and documentation improvements. Some bug fix highlights:
+Highlights:
+- Introduction of primitive persistent arrays in the core language, implemented using imperative persistent arrays.
+- Introduction of definitional proof irrelevance for the equality type defined in the SProp sort.
+- Many improvements to the handling of notations, including number notations, recursive notations and notations with bindings. A new algorithm chooses the most precise notation available to print an expression, which might introduce changes in printing behavior.
 
-- Polymorphic side-effects inside monomorphic definitions were incorrectly handled as not inlined. This allowed deriving an inconsistency (#13330).
-- 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` (#12837).
-- Several bugs with `Search` (#13298, #13349).
-- The `details` environment introduced in coqdoc in Coq 8.12 can now be used as advertised in the reference manual (#12772).
-- View menu "Display parentheses" introduced in CoqIDE in Coq 8.12 now works correctly (#12793).
-
-See the [changelog](https://coq.inria.fr/refman/changes.html#changes-in-8-12-1) for details and a more complete list.
-
-Note that we are not providing a macOS installer for this release due to infrastructure issues. We hope that this will be alleviated soon by the incoming [Coq Platform](https://github.com/coq/platform/). In the meantime, you can install Coq on macOS using `opam`, `nix` or `brew` (see [the wiki](https://github.com/coq/coq/wiki/Installation%20of%20Coq%20on%20Mac)).
+See the [changelog](https://coq.github.io/doc/v8.13/refman/changes.html#version-8-13) for an overview of the new features and changes.
 </releaseNotes>
     <dependencies>
       <dependency id="chocolatey-core.extension" version="1.3.3" />

automatic/coq/tools/chocolateyInstall.ps1

@@ -3,12 +3,12 @@
 $packageArgs = @{
   packageName    = $env:ChocolateyPackageName
   fileType       = 'exe'
-  url            = 'https://github.com/coq/coq/releases/download/V8.12.1/coq-8.12.1-installer-windows-i686.exe'
-  url64bit       = 'https://github.com/coq/coq/releases/download/V8.12.1/coq-8.12.1-installer-windows-x86_64.exe'
+  url            = 'https://github.com/coq/coq/releases/download/V8.13.0/coq-8.13.0-installer-windows-i686.exe'
+  url64bit       = 'https://github.com/coq/coq/releases/download/V8.13.0/coq-8.13.0-installer-windows-x86_64.exe'
   softwareName   = 'coq*'
-  checksum       = '6f1b06fd11a5e645613f08d742415a55f8d2bd27c2a762ecc73e7efae7bfb5b5'
+  checksum       = '0b32aae5048a84c838c42fbc88feb93c1fd17afb92f1b5ab82b9e364f070a897'
   checksumType   = 'sha256'
-  checksum64     = '6a287c3b7b783064485561386194c3460b30e7210cf315b95eaeb93402150680'
+  checksum64     = '717917b3b5c29b436f28d9b69f8dbf8751f09d1fa9d7376c3fc64ed4ab38a39d'
   checksumType64 = 'sha256'
   silentArgs     = '/S'
   validExitCodes = @(0)