Commit 1b8a2e50 authored by Ralf Jung's avatar Ralf Jung

add an omega auto database

parent 026cf958
......@@ -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]
......
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment