- Update to version 8.17.1.

* Fixed incorrect paths emitted by coqdep in some cases for META
    files which prevented dune builds for plugins from working
    correctly.
  * Fixed shadowing of record fields in extraction to OCaml.
  * Fixed an impossible-to-turn-off debug message "backtracking and
    redoing byextend on ...".
  * Fixed a major memory regression affecting MathComp 2.
- Classify desktop entry under Science instead of Education.
- Add screenshot URL to AppStream metadata.

OBS-URL: https://build.opensuse.org/package/show/science/coq?expand=0&rev=50

coq-8.17.0.tar.gz

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

coq-8.17.1.tar.gz

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

coq-refman-8.17.0.tar.xz

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

coq-refman-8.17.1.tar.xz

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

coq-stdlib-8.17.0.tar.xz

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

coq-stdlib-8.17.1.tar.xz

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

coq.changes

@@ -1,3 +1,17 @@
+-------------------------------------------------------------------
+Wed Jun 28 21:03:07 UTC 2023 - Aaron Puchert <aaronpuchert@alice-dsl.net>
+
+- Update to version 8.17.1.
+  * Fixed incorrect paths emitted by coqdep in some cases for META
+    files which prevented dune builds for plugins from working
+    correctly.
+  * Fixed shadowing of record fields in extraction to OCaml.
+  * Fixed an impossible-to-turn-off debug message "backtracking and
+    redoing byextend on ...".
+  * Fixed a major memory regression affecting MathComp 2.
+- Classify desktop entry under Science instead of Education.
+- Add screenshot URL to AppStream metadata.
+
 -------------------------------------------------------------------
 Tue Mar 28 21:18:57 UTC 2023 - Aaron Puchert <aaronpuchert@alice-dsl.net>
 

coq.spec

@@ -26,7 +26,7 @@
 %endif
 
 Name:           coq
-Version:        8.17.0
+Version:        8.17.1
 Release:        0
 Summary:        Proof Assistant based on the Calculus of Inductive Constructions
 License:        LGPL-2.1-only

fr.inria.coq.coqide.desktop

@@ -4,7 +4,7 @@ Type=Application
 Name=Coq IDE
 GenericName=Proof Assistant
 Comment=Proof Assistant based on the Calculus of Inductive Constructions
-Categories=Education;Science;Math;
+Categories=Science;Math;
 MimeType=text/x-coqsrc;
 Exec=coqide %F
 Icon=coq

fr.inria.coq.coqide.metainfo.xml

@@ -40,7 +40,7 @@
   <url type="homepage">https://coq.inria.fr/</url>
   <url type="bugtracker">https://github.com/coq/coq/issues</url>
   <url type="faq">https://github.com/coq/coq/wiki/The-Coq-FAQ</url>
-  <url type="help">https://coq.inria.fr/documentation</url>
+  <url type="help">https://coq.inria.fr/refman/practical-tools/coqide.html</url>
   <url type="donation">https://coq.inria.fr/consortium</url>
   <url type="vcs-browser">https://github.com/coq/coq</url>
   <url type="contribute">https://github.com/coq/coq/blob/master/CONTRIBUTING.md</url>
@@ -56,5 +56,12 @@
     <binary>coqide</binary>
   </provides>
   <project_license>LGPL-2.1-only</project_license>
+  <screenshots>
+    <screenshot type="default">
+      <image type="source">
+        https://coq.inria.fr/refman/_images/coqide.png
+      </image>
+    </screenshot>
+  </screenshots>
   <content_rating type="oars-1.1"/>
 </component>