Merge branch 'robbert/omega' into 'master'

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

See merge request !216

CHANGELOG.md

@@ -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`):

theories/tactics.v

 (** This file collects general purpose tactics that are used throughout
 the development. *)
-From Coq Require Import Omega.
 From Coq Require Export Lia.
 From stdpp Require Export decidable.
 From stdpp Require Import options.
@@ -24,7 +23,6 @@ to be combined in combination with other hint database. *)
 Global Hint Extern 998 (_ = _) => f_equal : f_equal.
 Global Hint Extern 999 => congruence : congruence.
 Global Hint Extern 1000 => lia : lia.
-Global Hint Extern 1000 => omega : omega.
 Global Hint Extern 1001 => progress subst : subst. (** backtracking on this one will
 be very bad, so use with care! *)