From 38417becf9810412ba2160ac829b7349893e8dbc Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Fri, 22 Jul 2016 14:53:22 +0200
Subject: [PATCH] More consistent file names for coPset, bset and set.

Similar files (gmap, listset, ...) were already in singular form and
matched the name of the set/map data type.
---
 _CoqProject                     | 6 +++---
 algebra/sts.v                   | 2 +-
 prelude/{bsets.v => bset.v}     | 0
 prelude/{co_pset.v => coPset.v} | 0
 prelude/gmap.v                  | 2 +-
 prelude/{sets.v => set.v}       | 0
 program_logic/namespaces.v      | 2 +-
 program_logic/pviewshifts.v     | 2 +-
 program_logic/wsat.v            | 2 +-
 9 files changed, 8 insertions(+), 8 deletions(-)
 rename prelude/{bsets.v => bset.v} (100%)
 rename prelude/{co_pset.v => coPset.v} (100%)
 rename prelude/{sets.v => set.v} (100%)

diff --git a/_CoqProject b/_CoqProject
index 7f98bf17f..000e00dbf 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -1,7 +1,7 @@
 -Q . iris
 prelude/option.v
 prelude/fin_map_dom.v
-prelude/bsets.v
+prelude/bset.v
 prelude/fin_maps.v
 prelude/vector.v
 prelude/pmap.v
@@ -28,9 +28,9 @@ prelude/finite.v
 prelude/numbers.v
 prelude/nmap.v
 prelude/zmap.v
-prelude/co_pset.v
+prelude/coPset.v
 prelude/lexico.v
-prelude/sets.v
+prelude/set.v
 prelude/decidable.v
 prelude/list.v
 prelude/error.v
diff --git a/algebra/sts.v b/algebra/sts.v
index 7950bf8cd..5be1a6574 100644
--- a/algebra/sts.v
+++ b/algebra/sts.v
@@ -1,4 +1,4 @@
-From iris.prelude Require Export sets.
+From iris.prelude Require Export set.
 From iris.algebra Require Export cmra.
 From iris.algebra Require Import dra.
 Local Arguments valid _ _ !_ /.
diff --git a/prelude/bsets.v b/prelude/bset.v
similarity index 100%
rename from prelude/bsets.v
rename to prelude/bset.v
diff --git a/prelude/co_pset.v b/prelude/coPset.v
similarity index 100%
rename from prelude/co_pset.v
rename to prelude/coPset.v
diff --git a/prelude/gmap.v b/prelude/gmap.v
index d72514bc2..bf74baaaf 100644
--- a/prelude/gmap.v
+++ b/prelude/gmap.v
@@ -3,7 +3,7 @@
 (** This file implements finite maps and finite sets with keys of any countable
 type. The implementation is based on [Pmap]s, radix-2 search trees. *)
 From iris.prelude Require Export countable fin_maps fin_map_dom.
-From iris.prelude Require Import pmap mapset sets.
+From iris.prelude Require Import pmap mapset set.
 
 (** * The data structure *)
 (** We pack a [Pmap] together with a proof that ensures that all keys correspond
diff --git a/prelude/sets.v b/prelude/set.v
similarity index 100%
rename from prelude/sets.v
rename to prelude/set.v
diff --git a/program_logic/namespaces.v b/program_logic/namespaces.v
index ee59788b1..02e2a8dd6 100644
--- a/program_logic/namespaces.v
+++ b/program_logic/namespaces.v
@@ -1,4 +1,4 @@
-From iris.prelude Require Export countable co_pset.
+From iris.prelude Require Export countable coPset.
 From iris.algebra Require Export base.
 
 Definition namespace := list positive.
diff --git a/program_logic/pviewshifts.v b/program_logic/pviewshifts.v
index df3207507..7df781061 100644
--- a/program_logic/pviewshifts.v
+++ b/program_logic/pviewshifts.v
@@ -1,4 +1,4 @@
-From iris.prelude Require Export co_pset.
+From iris.prelude Require Export coPset.
 From iris.algebra Require Export upred_big_op.
 From iris.program_logic Require Export model.
 From iris.program_logic Require Import ownership wsat.
diff --git a/program_logic/wsat.v b/program_logic/wsat.v
index 0392bd540..8e818b8c3 100644
--- a/program_logic/wsat.v
+++ b/program_logic/wsat.v
@@ -1,4 +1,4 @@
-From iris.prelude Require Export co_pset.
+From iris.prelude Require Export coPset.
 From iris.program_logic Require Export model.
 From iris.algebra Require Export cmra_big_op cmra_tactics.
 Local Hint Extern 10 (_ ≤ _) => omega.
-- 
GitLab