--- a/src/LogicProg.v	Sun Feb 02 10:51:18 2020 -0500
+++ b/src/LogicProg.v	Sun Jul 31 14:48:22 2022 -0400
@@ -9,7 +9,7 @@
 
 (* begin hide *)
 
-Require Import List Omega.
+Require Import List Lia.
 
 Require Import Cpdt.CpdtTactics.
 
@@ -152,7 +152,7 @@
 (** Sometimes it is useful to see a description of the proof tree that [auto] finds, with the %\index{tactics!info}%[info] tactical.  (This tactical is not available in Coq 8.4 as of this writing, but I hope it reappears soon.  The special case %\index{tactics!info\_auto}%[info_auto] tactic is provided as a chatty replacement for [auto].) *)
 
 Restart.
-  info auto 6.
+  info_auto 6.
 (** %\vspace{-.15in}%[[
  == apply PlusS; apply PlusS; apply PlusS; apply PlusS; 
     apply PlusS; apply PlusO.
@@ -220,7 +220,7 @@
 (** The [auto] tactic will not perform these sorts of steps that introduce unification variables, but the %\index{tactics!eauto}%[eauto] tactic will.  It is helpful to work with two separate tactics, because proof search in the [eauto] style can uncover many more potential proof trees and hence take much longer to run. *)
 
 Restart.
-  info eauto 6.
+  info_eauto 6.
 (** %\vspace{-.15in}%[[
  == eapply ex_intro; apply PlusS; apply PlusS; 
     apply PlusS; apply PlusS; apply PlusO.
@@ -431,7 +431,7 @@
   -> y = 2
   -> exists z, z + x = 3.
 (* begin thide *)
-  info eauto with slow.
+  info_eauto with slow.
 (** %\vspace{-.2in}%[[
  == intro x; intro y; intro H; intro H0; simple eapply ex_intro; 
     apply plusS; simple eapply eq_trans.
@@ -672,9 +672,9 @@
 
 Hint Resolve EvalPlus'.
 
-(** Further, we instruct [eauto] to apply %\index{tactics!omega}%[omega], a standard tactic that provides a complete decision procedure for quantifier-free linear arithmetic.  Via [Hint Extern], we ask for use of [omega] on any equality goal.  The [abstract] tactical generates a new lemma for every such successful proof, so that, in the final proof term, the lemma may be referenced in place of dropping in the full proof of the arithmetic equality. *)
+(** Further, we instruct [eauto] to apply %\index{tactics!lia}%[lia], a standard tactic that provides a complete decision procedure for quantifier-free linear arithmetic.  Via [Hint Extern], we ask for use of [lia] on any equality goal.  The [abstract] tactical generates a new lemma for every such successful proof, so that, in the final proof term, the lemma may be referenced in place of dropping in the full proof of the arithmetic equality. *)
 
-Hint Extern 1 (_ = _) => abstract omega.
+Hint Extern 1 (_ = _) => abstract lia.
 (* end thide *)
 
 (** Now we can return to [eval1'] and prove it automatically. *)
@@ -696,7 +696,7 @@
 ]]
 *)
 
-(** The lemma [eval1'_subproof] was generated by [abstract omega].
+(** The lemma [eval1'_subproof] was generated by [abstract lia].
 
    Now we are ready to take advantage of logic programming's flexibility by searching for a program (arithmetic expression) that always evaluates to a particular symbolic value. *)