From c366c8f59b4e3443938b9f2bffe6d43948b426f3 Mon Sep 17 00:00:00 2001
From: Dan Frumin <dfrumin@cs.ru.nl>
Date: Sat, 10 Feb 2018 20:06:37 +0100
Subject: [PATCH] Use the namespace FSets

---
 FiniteSets/CPP.v                 | 6 +++---
 FiniteSets/_CoqProject           | 5 ++++-
 FiniteSets/fincard.v             | 4 ++--
 FiniteSets/subobjects/b_finite.v | 2 +-
 4 files changed, 10 insertions(+), 7 deletions(-)

diff --git a/FiniteSets/CPP.v b/FiniteSets/CPP.v
index 11d8d6a..da7dd3d 100644
--- a/FiniteSets/CPP.v
+++ b/FiniteSets/CPP.v
@@ -1,7 +1,7 @@
 Require Import FSets list_representation.
 Require Import kuratowski.length misc.dec_kuratowski.
-From interfaces Require Import lattice_interface.
-From subobjects Require Import sub b_finite enumerated k_finite.
+From FSets.interfaces Require Import lattice_interface.
+From FSets.subobjects Require Import sub b_finite enumerated k_finite.
 
 (** * Definitions *)
 Definition definition_2_1 := FSet.
@@ -105,7 +105,7 @@ Definition proposition_4_22 `{Univalence} := bfin_to_kfin.
 Definition theorem_4_23 `{Univalence} (X : Type) `{DecidablePaths X} := Kf_to_Bf X.
 
 (** * Interface for finite sets *)
-From interfaces Require Import set_interface.
+From FSets.interfaces Require Import set_interface.
 (** ** Method *)
 Definition definition_5_1 := tt. (* not actually present; bundled in the next definition *)
 Definition definition_5_2 `{Univalence} := sets.
diff --git a/FiniteSets/_CoqProject b/FiniteSets/_CoqProject
index 1b6fd62..a4dae64 100644
--- a/FiniteSets/_CoqProject
+++ b/FiniteSets/_CoqProject
@@ -1,4 +1,6 @@
--R . "" COQC = hoqc COQDEP = hoqdep
+-R . FSets
+COQC = hoqc
+COQDEP = hoqdep
 HitTactics.v
 prelude.v
 interfaces/lattice_interface.v
@@ -28,3 +30,4 @@ misc/dec_kuratowski.v
 misc/dec_fset.v
 implementations/lists.v
 CPP.v
+fincard.v
diff --git a/FiniteSets/fincard.v b/FiniteSets/fincard.v
index 85ba9c0..0754275 100644
--- a/FiniteSets/fincard.v
+++ b/FiniteSets/fincard.v
@@ -1,7 +1,7 @@
 Require Import FSets list_representation.
 Require Import kuratowski.length misc.dec_kuratowski.
-From interfaces Require Import lattice_interface.
-From subobjects Require Import sub b_finite enumerated k_finite.
+From FSets.interfaces Require Import lattice_interface.
+From FSets.subobjects Require Import sub b_finite enumerated k_finite.
 
 Require Import HoTT.Spaces.Card.
 
diff --git a/FiniteSets/subobjects/b_finite.v b/FiniteSets/subobjects/b_finite.v
index 6b30dbe..3082826 100644
--- a/FiniteSets/subobjects/b_finite.v
+++ b/FiniteSets/subobjects/b_finite.v
@@ -1,7 +1,7 @@
 (* Bishop-finiteness is that "default" notion of finiteness in the HoTT library *)
 Require Import HoTT HitTactics.
 Require Import FSets interfaces.lattice_interface.
-From subobjects Require Import sub k_finite.
+From FSets.subobjects Require Import sub k_finite.
 
 Section finite_hott.
   Variable (A : Type).