# The reference omega was not found in the current environment
**URL:** https://discourse.rocq-prover.org/t/the-reference-omega-was-not-found-in-the-current-environment/1743
**Category:** Using Rocq
**Tags:** software-foundations
**Created:** [July 31, 2022, 7:50am UTC](https://discourse.rocq-prover.org/t/the-reference-omega-was-not-found-in-the-current-environment/1743 "2022-07-31T07:50:07Z")
**Posts on this page:** 3
**Page:** 1
### Author:  [@LuoYI](https://discourse.rocq-prover.org/u/LuoYI)
#### Post date: [July 31, 2022, 7:50am UTC](https://discourse.rocq-prover.org/t/the-reference-omega-was-not-found-in-the-current-environment/1743/1 "2022-07-31T07:50:07Z")
I am reading Software Foundation and it used tactic “omega” in a proof. But coq says “The reference omega was not found in the current environment.” There are only OmegaLemmas and PreOmega under “coq-platform\lib\coq\theories\omega”
---
### Author:  [@casteran](https://discourse.rocq-prover.org/u/casteran)
#### Post date: [July 31, 2022, 11:02am UTC](https://discourse.rocq-prover.org/t/the-reference-omega-was-not-found-in-the-current-environment/1743/2 "2022-07-31T11:02:42Z")
`omega` is deprecated in favor of the `lia` tactic (see [Omega: a (deprecated) solver for arithmetic — Coq 8.13.2 documentation](https://coq.github.io/doc/v8.13/refman/addendum/omega.html)).
Just do `Require Import Lia` in order to use it.
---
### Author:  [@bcpierce](https://discourse.rocq-prover.org/u/bcpierce)
#### Post date: [August 1, 2022, 3:19pm UTC](https://discourse.rocq-prover.org/t/the-reference-omega-was-not-found-in-the-current-environment/1743/3 "2022-08-01T15:19:37Z")
The next SF release (coming in the next few days) will remove Omega completely.