- Update to version 8.11.2.

* Fixed a kernel issue where using Require inside a section
    caused an anomaly when closing the section.
  * Fixed normalization in conclusion of custom induction scheme.
  * Fixed a loss of location of some tactic errors.
  * Ignore -native-compiler option when built without native
    compute support.
  * Fixed a segfault issue with CoqIDE completion.
  * Highlighting style is now consistently applied to all three
    buffers of CoqIDE.

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

coq-8.11.1.tar.gz

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

coq-8.11.2.tar.gz

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

coq.changes

@@ -1,3 +1,17 @@
+-------------------------------------------------------------------
+Sat Jun  6 12:11:06 UTC 2020 - Aaron Puchert <aaronpuchert@alice-dsl.net>
+
+- Update to version 8.11.2.
+  * Fixed a kernel issue where using Require inside a section
+    caused an anomaly when closing the section.
+  * Fixed normalization in conclusion of custom induction scheme.
+  * Fixed a loss of location of some tactic errors.
+  * Ignore -native-compiler option when built without native
+    compute support.
+  * Fixed a segfault issue with CoqIDE completion.
+  * Highlighting style is now consistently applied to all three
+    buffers of CoqIDE.
+
 -------------------------------------------------------------------
 Wed Apr  8 22:20:23 UTC 2020 - Aaron Puchert <aaronpuchert@alice-dsl.net>
 

coq.spec

@@ -18,7 +18,7 @@
 
 
 Name:           coq
-Version:        8.11.1
+Version:        8.11.2
 Release:        0
 Summary:        Proof Assistant based on the Calculus of Inductive Constructions
 License:        LGPL-2.1-only