Skip to content
Snippets Groups Projects
Commit 59af581a authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Remove obsolete remark, `omega` has been removed in Coq 8.14.

parent 22151b7b
No related branches found
No related tags found
1 merge request!473Take advantage of new Coq features in Coq 8.15
Hide whitespace changes
Inline Side-by-side
Showing
with 0 additions and 4 deletions
README.md
+ 0
− 4
View file @ 59af581a
...@@ -36,10 +36,6 @@ Notably: ...@@ -36,10 +36,6 @@ Notably:
* It blocks `simpl` on all operations involving integers `Z` (by setting * It blocks `simpl` on all operations involving integers `Z` (by setting
`Arguments op : simpl never`). We do this because `simpl` tends to expose `Arguments op : simpl never`). We do this because `simpl` tends to expose
the internals of said operations (e.g. try `simpl` on `Z.of_nat (S n) + y`). the internals of said operations (e.g. try `simpl` on `Z.of_nat (S n) + y`).
As a consequence of blocking `simpl`, due to
[Coq bug #5039](https://github.com/coq/coq/issues/5039) the `omega` tactic
becomes unreliable. We do not consider this an issue since we use `lia` (for
which the aforementioned Coq bug was fixed) instead of `omega` everywhere.
## Prerequisites ## Prerequisites
......
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment