SHA256
1
0
forked from pool/coq
Commit Graph

2 Commits

Author SHA256 Message Date
Aaron Puchert
edfae7dd86 - 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
2023-06-28 23:04:37 +00:00
Aaron Puchert
9b2016e937 - Update to version 8.15.2.
* Tactics `intuition` and `dintuition` use
    `Tauto.intuition_solver` (defined as `auto with *`) instead of
    hardcoding `auto with *`. This makes it possible to change the
    default solver with `Ltac Tauto.intuition_solver ::= ...`.
  * Fixed an uncaught exception `UnableToUnify` with
    bidirectionality hints.
  * Fixed multiple CoqIDE bugs.
  * Fixed an incorrect implementation of `SFClassify`, allowing for
    a proof of `False` since 8.11.0, due to Axioms present in
    `Float.Axioms`.
- Rename coq.desktop to fr.inria.coq.coqide.desktop as the
  documentation suggests, add an accompanying metainfo file.
- Declare documentation as noarch.

OBS-URL: https://build.opensuse.org/package/show/science/coq?expand=0&rev=40
2022-06-01 21:48:29 +00:00