SHA256
1
0
forked from pool/coq
Commit Graph

1 Commits

Author SHA256 Message Date
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