Skip to content
Snippets Groups Projects

Remove hint db and import of omega, since omega will be removed from Coq.

Merged Remove hint db and import of omega, since omega will be removed from Coq.
robbert/omega into master
Merged Robbert Krebbers requested to merge robbert/omega into master
Compare
and
2 files
+ 1
− 2
Compare changes
  • Side-by-side
  • Inline
Files
2
CHANGELOG.md
+ 1
− 0
@@ -42,6 +42,7 @@ Coq 8.8 and 8.9 are no longer supported.
`map_fmap_empty_inv` into `fmap_empty_inv` for consistency's sake.
- Rename `seq_S_end_app` to `seq_S`. (The lemma `seq_S` is also in Coq's stdlib
since Coq 8.12.)
- Remove `omega` import and hint database in `tactics` file.
The following `sed` script should perform most of the renaming
(on macOS, replace `sed` by `gsed`, installed via e.g. `brew install gnu-sed`):