fix 8.12 errors and deprecations

Author: palmskog

Examples/TwoPhaseCommit/TwoPhaseCoordinator.v

@@ -67,7 +67,7 @@ Next Obligation. by case/andP: H=>/eqP->_; rewrite /ddom domPt inE/=. Qed.
 (************** Coordinator code **************)
 
 (*** Reading internal state ***)
-Arguments TPCProtocol.TPCCoh [cn pts others].
+Arguments TPCProtocol.TPCCoh {cn pts others}.
 Notation coh := (@TPCProtocol.TPCCoh cn pts others).
 Notation getS s := (getStatelet s l).
 Notation loc i := (getLocal cn (getStatelet i l)).

Examples/TwoPhaseCommit/TwoPhaseInductiveInv.v

@@ -15,7 +15,7 @@ Require Import InductiveInv While StatePredicates.
 From DiSeL
 Require Import TwoPhaseProtocol.
 
-Require Import Omega.
+Require Import Lia.
 
 Set Implicit Arguments.
 Unset Strict Implicit.
@@ -2027,7 +2027,7 @@ case.
   match goal with
   | [ H : pt_state _ _ _ _ |- _ ] =>
     move: H =>/(pt_state_functional V' PS')[]; try discriminate
-  end; case; intros; subst; auto; try omega.
+  end; case; intros; subst; auto; try lia.
 Qed.
 
 Lemma cn_log_agreement d r lg pt :