fix final deprecation warnings

Author: palmskog

Examples/Calculator/CalculatorClientLib.v

@@ -11,7 +11,7 @@ Require Import Freshness State EqTypeX Protocols Worlds NetworkSem Rely.
 From DiSeL
 Require Import Actions Injection Process Always HoareTriples InferenceRules.
 From DiSeL
-Require Import InductiveInv.
+Require Import InductiveInv While.
 From DiSeL
 Require Import CalculatorProtocol CalculatorInvariant.
 From DiSeL
@@ -133,9 +133,6 @@ Definition receive_loop_inv (rs : reqs) :=
      | None => loc i = st :-> rs
     end.
 
-From DiSeL
-Require Import While.
-
 Program Definition receive_loop' :
   {(rs : reqs)}, DHT [cl, W]
   (fun i => loc i = st :-> rs,

Examples/Calculator/CalculatorInvariant.v

@@ -59,8 +59,6 @@ Notation coh' := (coh cal).
 Notation Sinv := (@S_inv cal (fun d _ => CalcInv d)).
 Notation Rinv := (@R_inv cal (fun d _ => CalcInv d)).
 Notation PI := pf_irr.
-From DiSeL
-Require Import CalculatorProtocol.
 
 Program Definition s1: Sinv (server_send_trans f prec cs cls).
 Proof.

Examples/Calculator/CalculatorServerLib.v

@@ -11,7 +11,7 @@ Require Import Freshness State EqTypeX Protocols Worlds NetworkSem Rely.
 From DiSeL
 Require Import Actions Injection Process Always HoareTriples InferenceRules.
 From DiSeL
-Require Import InductiveInv.
+Require Import InductiveInv While.
 From DiSeL
 Require Import CalculatorProtocol CalculatorInvariant.
 From DiSeL
@@ -92,9 +92,6 @@ Definition receive_req_loop_inv (ps : reqs) :=
      | None => loc i = st :-> ps
     end.
 
-From DiSeL
-Require Import While.
-
 Program Definition receive_req_loop :
   {ps : reqs}, DHT [sv, W]
   (fun i => loc i = st :-> ps,

Examples/Querying/QueryHooked.v

@@ -1,18 +1,14 @@
 From mathcomp.ssreflect
-Require Import ssreflect ssrbool ssrnat eqtype ssrfun seq.
-From mathcomp
-Require Import path.
+Require Import ssreflect ssrbool ssrnat eqtype ssrfun seq path.
 Require Import Eqdep.
 From fcsl
 Require Import axioms pred prelude ordtype finmap pcm unionmap heap.
 From DiSeL
 Require Import Freshness State EqTypeX Protocols Worlds NetworkSem Rely Actions.
 From DiSeL
-Require Import SeqLib QueryProtocol.
+Require Import SeqLib QueryProtocol NewStatePredicates Actions.
 From DiSeL
-Require Import NewStatePredicates.
-From DiSeL
-Require Import Actions Injection Process Always HoareTriples InferenceRules.
+Require Import Injection Process Always HoareTriples InferenceRules While.
 
 Section QueryHooked.
 
@@ -1080,9 +1076,6 @@ Definition recv_resp_inv (rid : nat) to
           local_indicator data (getLc i) &
           msg_story i rid to data ((to, rid) :: reqs) resp].
 
-From DiSeL
-Require Import While.
-
 Program Definition receive_resp_loop (rid : nat) to :
   {(rrd : (seq (nid * nat) * seq (nid * nat) * Data))}, DHT [this, W]
   (fun i => let: (reqs, resp, data) := rrd in
@@ -1245,4 +1238,3 @@ by apply: (core_state_stable _ _ _ _ R _ T2 T4); case: T3.
 Qed.
 
 End QueryHooked.
-

Examples/TwoPhaseCommit/TwoPhaseParticipant.v

@@ -85,7 +85,7 @@ Next Obligation. by rewrite !InE; do![right]. Qed.
 
 (************** Participant code **************)
 
-Implicit 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 p (getStatelet i l)).