Commit 38417bec authored by Robbert Krebbers's avatar Robbert Krebbers

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.
parent ae65433f
-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
......
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 _ _ !_ /.
......
......@@ -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
......
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.
......
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.
......
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.
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment