From 1b8a2e50d8174ebaf943defe38448946d73ab9c7 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Tue, 2 Feb 2016 23:01:29 +0100
Subject: [PATCH] add an omega auto database

---
 theories/tactics.v | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/theories/tactics.v b/theories/tactics.v
index 85c0fd52..d5867ab6 100644
--- a/theories/tactics.v
+++ b/theories/tactics.v
@@ -2,6 +2,7 @@
 (* This file is distributed under the terms of the BSD license. *)
 (** This file collects general purpose tactics that are used throughout
 the development. *)
+Require Import Omega.
 Require Export Psatz.
 Require Export prelude.base.
 
@@ -24,6 +25,7 @@ to be combined in combination with other hint database. *)
 Hint Extern 998 (_ = _) => f_equal : f_equal.
 Hint Extern 999 => congruence : congruence.
 Hint Extern 1000 => lia : lia.
+Hint Extern 1000 => omega : omega.
 
 (** The tactic [intuition] expands to [intuition auto with *] by default. This
 is rather efficient when having big hint databases, or expensive [Hint Extern]
-- 
GitLab