diff --git a/SConstruct b/SConstruct
index 00d1637d796d9ae723bb3e5c29ca2bbb8548852b..248886fb06f2d19d1821b9058b211b2c054f80bc 100644
--- a/SConstruct
+++ b/SConstruct
@@ -2,7 +2,7 @@
 # This file is distributed under the terms of the BSD license.
 import os, glob, string
 
-modules = ["prelude", "iris"]
+modules = ["prelude", "modures", "iris"]
 Rs = '-Q . ""'
 env = DefaultEnvironment(ENV = os.environ,tools=['default', 'Coq'], COQFLAGS=Rs)
 
diff --git a/modures/agree.v b/modures/agree.v
index 41f991216db5e2d1ea89891e9f3972cbcdf89579..1af18cfbe42bee1ec1f994ea5eecb6a16a016d35 100644
--- a/modures/agree.v
+++ b/modures/agree.v
@@ -1,4 +1,4 @@
-Require Export iris.cmra.
+Require Export modures.cmra.
 Local Hint Extern 10 (_ ≤ _) => omega.
 
 Record agree A `{Dist A} := Agree {
diff --git a/modures/auth.v b/modures/auth.v
index d29b6744a2f962e02a8947db821b88cbb6a19100..3f4fcebe3eaddbe4f84893c7ba915c6beee01520 100644
--- a/modures/auth.v
+++ b/modures/auth.v
@@ -1,4 +1,4 @@
-Require Export iris.excl.
+Require Export modures.excl.
 Local Arguments valid _ _ !_ /.
 Local Arguments validN _ _ _ !_ /.
 
diff --git a/modures/cmra.v b/modures/cmra.v
index 73b49da8bef33a97bc05b65fbfdee29d5bb2908e..1e67403d925ca2cbcdf6ceedcee917dd5b3cbfda 100644
--- a/modures/cmra.v
+++ b/modures/cmra.v
@@ -1,4 +1,4 @@
-Require Export iris.ra iris.cofe.
+Require Export modures.ra modures.cofe.
 
 Class ValidN (A : Type) := validN : nat → A → Prop.
 Instance: Params (@validN) 3.
diff --git a/modures/cmra_maps.v b/modures/cmra_maps.v
index 522ed2ec415b2618ba5cb8a4d1e01fbff9dfcb2e..966db0da7fe279e21737f638f4b97f7b0be74126 100644
--- a/modures/cmra_maps.v
+++ b/modures/cmra_maps.v
@@ -1,4 +1,4 @@
-Require Export iris.cmra iris.cofe_maps.
+Require Export modures.cmra modures.cofe_maps.
 Require Import prelude.pmap prelude.natmap prelude.gmap.
 
 (** option *)
diff --git a/modures/cofe_maps.v b/modures/cofe_maps.v
index 7a3a2100a7418a5a500812d135ed52896288aa49..c421ccd534a8a0bfc7520a80e3a0dc4701a4a6a0 100644
--- a/modures/cofe_maps.v
+++ b/modures/cofe_maps.v
@@ -1,4 +1,4 @@
-Require Export iris.cofe prelude.fin_maps.
+Require Export modures.cofe prelude.fin_maps.
 Require Import prelude.pmap prelude.gmap prelude.natmap.
 Local Obligation Tactic := idtac.
 
diff --git a/modures/cofe_solver.v b/modures/cofe_solver.v
index 0610e1f3d02fd484c5f9b67f63bd39b9085527ad..9517223b5b2fd03a9eb368c00fff2087ff025f95 100644
--- a/modures/cofe_solver.v
+++ b/modures/cofe_solver.v
@@ -1,4 +1,4 @@
-Require Export iris.cofe.
+Require Export modures.cofe.
 
 Section solver.
 Context (F : cofeT → cofeT → cofeT).
diff --git a/modures/dra.v b/modures/dra.v
index 993b36be591bf01cb7a3bd91cc148f840a93106c..20d73cb0a72b26a2184627da9a964ca2fa647916 100644
--- a/modures/dra.v
+++ b/modures/dra.v
@@ -1,4 +1,4 @@
-Require Export iris.ra iris.cmra.
+Require Export modures.ra modures.cmra.
 
 (** From disjoint pcm *)
 Record validity {A} (P : A → Prop) : Type := Validity {
diff --git a/modures/excl.v b/modures/excl.v
index 53c63b150f3b3a6365b2f597fa21ce5222891201..09b8f032ed1b189d5222bb7e0dd8cae414c563e7 100644
--- a/modures/excl.v
+++ b/modures/excl.v
@@ -1,4 +1,4 @@
-Require Export iris.cmra.
+Require Export modures.cmra.
 Local Arguments validN _ _ _ !_ /.
 Local Arguments valid _ _  !_ /.
 
diff --git a/modures/logic.v b/modures/logic.v
index fa24ea6046394cd0fa512b5227b44343092b43ca..2c36c23038f2e4d8177fb38de5c19c6288643124 100644
--- a/modures/logic.v
+++ b/modures/logic.v
@@ -1,4 +1,4 @@
-Require Import iris.cmra.
+Require Import modures.cmra.
 Local Hint Extern 1 (_ ≼ _) => etransitivity; [eassumption|].
 Local Hint Extern 1 (_ ≼ _) => etransitivity; [|eassumption].
 Local Hint Extern 10 (_ ≤ _) => omega.
diff --git a/modures/sts.v b/modures/sts.v
index f98c874639df054eae6179883e95e9c7f5ed906f..aee7969f19e3489f00bb31958771b5f08346dd6b 100644
--- a/modures/sts.v
+++ b/modures/sts.v
@@ -1,5 +1,5 @@
-Require Export iris.ra.
-Require Import prelude.sets iris.dra.
+Require Export modures.ra.
+Require Import prelude.sets modures.dra.
 Local Arguments valid _ _ !_ /.
 Local Arguments op _ _ !_ !_ /.
 Local Arguments unit _ _ !_ /.