diff --git a/structures.v b/HB/structures.v
similarity index 100%
rename from structures.v
rename to HB/structures.v
diff --git a/Makefile.coq.local b/Makefile.coq.local
index fdbf8849..564c569b 100644
--- a/Makefile.coq.local
+++ b/Makefile.coq.local
@@ -1,5 +1,5 @@
 # Coq does not know about Elpi Accumulate File, so we declare the dependency here
-structures.vo : $(wildcard HB/*.elpi HB/common/*.elpi)
+HB/structures.vo : $(wildcard HB/*.elpi HB/common/*.elpi)
 
 clean::
 	$(SHOW)'CLEAN *.hb *.hb.old'
diff --git a/_CoqProject b/_CoqProject
index 057e9001..b2e67cab 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -1,7 +1,7 @@
-structures.v
+HB/structures.v
 -arg -w -arg -elpi.accumulate-syntax
 -arg -w -arg +elpi.typecheck
--Q . HB
+-Q HB HB
 
 -R tests HB.tests
--R examples HB.examples
\ No newline at end of file
+-R examples HB.examples
diff --git a/_CoqProject.test-suite b/_CoqProject.test-suite
index f59e999a..e24fb2b3 100644
--- a/_CoqProject.test-suite
+++ b/_CoqProject.test-suite
@@ -100,4 +100,4 @@ tests/saturate_on.v
 -R tests HB.tests
 -R examples HB.examples
 
--Q . HB
\ No newline at end of file
+-Q HB HB