From 1c2e689101c0c6c533606338efbd3592c97c95e7 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Tue, 19 Jan 2021 11:51:44 +0100
Subject: [PATCH] Remove hint db and import of omega, since omega will be
 removed from Coq.

See https://github.com/coq/coq/pull/13741#issuecomment-762761112
---
 theories/tactics.v | 2 --
 1 file changed, 2 deletions(-)

diff --git a/theories/tactics.v b/theories/tactics.v
index 47401180..b635bdf7 100644
--- a/theories/tactics.v
+++ b/theories/tactics.v
@@ -1,6 +1,5 @@
 (** 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! *)
 
-- 
GitLab