diff options
| author | Jim Fehrle | 2021-01-11 14:47:13 -0800 |
|---|---|---|
| committer | Jim Fehrle | 2021-04-02 18:52:59 -0700 |
| commit | d3a51ac24244f586dfeff1a93b68cb084370534e (patch) | |
| tree | 99559dce00d49471fdea5deaff58e0dab481d941 /doc/sphinx/proof-engine | |
| parent | 012b8a08f142d39b2211fd52c811f830f88f2075 (diff) | |
Remove the omega tactic and related options
Diffstat (limited to 'doc/sphinx/proof-engine')
| -rw-r--r-- | doc/sphinx/proof-engine/ltac.rst | 9 |
1 files changed, 4 insertions, 5 deletions
diff --git a/doc/sphinx/proof-engine/ltac.rst b/doc/sphinx/proof-engine/ltac.rst index b1759bf71b..88fca93547 100644 --- a/doc/sphinx/proof-engine/ltac.rst +++ b/doc/sphinx/proof-engine/ltac.rst @@ -1666,7 +1666,7 @@ Proving a subgoal as a separate lemma: abstract is chosen to get a fresh name. If the proof is closed with :cmd:`Qed`, the auxiliary lemma is inlined in the final proof term. - This is useful with tactics such as :tacn:`omega` or + This is useful with tactics such as :tacn:`discriminate` that generate huge proof terms with many intermediate goals. It can significantly reduce peak memory use. In most cases it doesn't have a significant impact on run time. One case in which it can reduce run time @@ -2317,11 +2317,10 @@ performance issue. .. coqtop:: reset in - Set Warnings "-omega-is-deprecated". - Require Import Coq.omega.Omega. + Require Import Lia. Ltac mytauto := tauto. - Ltac tac := intros; repeat split; omega || mytauto. + Ltac tac := intros; repeat split; lia || mytauto. Notation max x y := (x + (y - x)) (only parsing). @@ -2340,7 +2339,7 @@ performance issue. Set Ltac Profiling. tac. Show Ltac Profile. - Show Ltac Profile "omega". + Show Ltac Profile "lia". .. coqtop:: in |