Merge pull request #6 from DistributedComponents/fix-require-deprecation

move Requires outside modules to avoid deprecation warnings

Author: ilyasergey

Core/Actions.v

@@ -8,6 +8,7 @@ From DiSeL.Heaps
 Require Import pred prelude idynamic ordtype finmap pcm unionmap heap coding.
 From DiSeL.Core
 Require Import Freshness State EqTypeX Protocols Worlds NetworkSem.
+Require Classical_Prop.
 
 Set Implicit Arguments.
 Unset Strict Implicit.
@@ -177,7 +178,7 @@ Definition tryrecv_act_step s1 s2 (r : option (nid * nat * seq nat)) :=
       s2 = upd l (DStatelet f' s') s1 &
       r = Some (from, tag tms, tms_cont tms)]).
 
-Require Import Classical_Prop.
+Import Classical_Prop.
 
 Lemma tryrecv_act_step_total s:
   tryrecv_act_safe s -> exists s' r , tryrecv_act_step s s' r.

Core/Always.v

@@ -10,6 +10,8 @@ From DiSeL.Core
 Require Import Freshness State EqTypeX DepMaps Protocols Worlds NetworkSem Rely.
 From DiSeL.Core
 Require Import Actions Injection Process.
+From DiSeL.Core
+Require InductiveInv.
 
 Set Implicit Arguments.
 Unset Strict Implicit.
@@ -456,11 +458,9 @@ End AlwaysInject.
 Notation alwsafe_sc s p scs := (always_sc s p scs (fun _ _ => True)).
 Notation alwsafe s p := (always s p (fun _ _ => True)).
 
-
 Module AlwaysInductiveInv.
 Section AlwaysInductiveInv.
-From DiSeL.Core
-Require Import InductiveInv.
+Import InductiveInv.
 Variable pr : protocol.
 
 (* Decompose the initial protocol *)

Core/InductiveInv.v

@@ -10,6 +10,7 @@ From DiSeL.Core
 Require Import Freshness State EqTypeX.
 From DiSeL.Core
 Require Import Protocols Worlds NetworkSem Rely.
+Require FunctionalExtensionality.
 Set Implicit Arguments.
 Unset Strict Implicit.
 Unset Printing Implicit Defensive.
@@ -194,7 +195,7 @@ Definition stsI sts := map (fun stt =>
 Definition rtsI rts := map (fun rtt =>
                           @rcv_transI (rt rtt) (@rt_inv rtt)) rts.
 
-Require Import Coq.Logic.FunctionalExtensionality.
+Import FunctionalExtensionality.
 
 Variable ii : InductiveInv.