From 789b377b03ce455ddd646349312923f96efeda21 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Tue, 15 Dec 2015 15:25:06 +0100
Subject: [PATCH] Fix namespaces after previous rename.

---
 SConstruct            | 2 +-
 modures/agree.v       | 2 +-
 modures/auth.v        | 2 +-
 modures/cmra.v        | 2 +-
 modures/cmra_maps.v   | 2 +-
 modures/cofe_maps.v   | 2 +-
 modures/cofe_solver.v | 2 +-
 modures/dra.v         | 2 +-
 modures/excl.v        | 2 +-
 modures/logic.v       | 2 +-
 modures/sts.v         | 4 ++--
 11 files changed, 12 insertions(+), 12 deletions(-)

diff --git a/SConstruct b/SConstruct
index 00d1637d7..248886fb0 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 41f991216..1af18cfbe 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 d29b6744a..3f4fcebe3 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 73b49da8b..1e67403d9 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 522ed2ec4..966db0da7 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 7a3a2100a..c421ccd53 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 0610e1f3d..9517223b5 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 993b36be5..20d73cb0a 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 53c63b150..09b8f032e 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 fa24ea604..2c36c2303 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 f98c87463..aee7969f1 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 _ _ !_ /.
-- 
GitLab