diff --git a/Makefile.coq.local b/Makefile.coq.local
index 6f9145f1b8..e4c4970959 100644
--- a/Makefile.coq.local
+++ b/Makefile.coq.local
@@ -57,7 +57,7 @@ CORE_DPDFILES=$(patsubst theories.%,file-dep-graphs/HoTT.%,$(subst /,.,$(CORE_VF
 # The list of files from contrib
 CONTRIB_VOFILES=$(CONTRIB_VFILES:.v=.$(VO))
 CONTRIB_GLOBFILES=$(CONTRIB_VFILES:.v=.glob)
-CONTRIB_HTMLFILES=$(patsubst contrib.%,html/HoTT.Contrib.%,$(subst /,.,$(CONTRIB_VFILES:.v=.html)))
+CONTRIB_HTMLFILES=$(patsubst contrib.%,html/HoTT_Contrib.%,$(subst /,.,$(CONTRIB_VFILES:.v=.html)))
 CONTRIB_TIMING_HTMLFILES=$(patsubst html/%,timing-html/%,$(CONTRIB_HTMLFILES))
 
 # I'm not sure why we needs = rather than :=, but we seem to
@@ -160,7 +160,7 @@ $(CORE_TIMING_HTMLFILES) $(CATEGORY_TIMING_HTMLFILES): timing-html/HoTT.%.html :
 	$(SHOW)'TIME2HTML HoTT.$* > $@'
 	$(HIDE) etc/time2html "$(<:.vo=.v.timing)" "$(<:.vo=.v)" > $@
 
-$(CONTRIB_TIMING_HTMLFILES): timing-html/HoTT.Contrib.%.html : contrib/$$(subst .,/,$$*).vo etc/time2html
+$(CONTRIB_TIMING_HTMLFILES): timing-html/HoTT_Contrib.%.html : contrib/$$(subst .,/,$$*).vo etc/time2html
 	@ mkdir -p $(dir $@)
 	$(SHOW)'TIME2HTML $* > $@'
 	$(HIDE) etc/time2html "$(<:.vo=.v.timing)" "$(<:.vo=.v)" > $@
diff --git a/contrib/dune b/contrib/dune
index 9e6b188832..7af7a5a7a5 100644
--- a/contrib/dune
+++ b/contrib/dune
@@ -1,4 +1,4 @@
 (coq.theory
- (name HoTT.Contrib)
+ (name HoTT_Contrib)
  (package coq-hott)
  (theories HoTT))
diff --git a/dune b/dune
index 7b6c83f780..993de9c994 100644
--- a/dune
+++ b/dune
@@ -32,10 +32,10 @@
    HoTT
    -Q
    contrib
-   HoTT.Contrib
+   HoTT_Contrib
    -Q
    test
-   HoTT.Tests
+   HoTT_Tests
    %{deps}
    -o)))
 
diff --git a/etc/generate_coqproject.sh b/etc/generate_coqproject.sh
index 4861dab9e5..413af0237a 100755
--- a/etc/generate_coqproject.sh
+++ b/etc/generate_coqproject.sh
@@ -25,8 +25,8 @@ COQPROJECT_HEADER=\
 # found in etc/. It is set to be untracked by git.
 ###############################################################################
 -R theories HoTT
--Q contrib HoTT.Contrib
--Q test HoTT.Tests
+-Q contrib HoTT_Contrib
+-Q test HoTT_Tests
 
 -arg -noinit
 -arg -indices-matter
@@ -38,8 +38,8 @@ if [ "$GENERATE_COQPROJECT_FOR_DUNE" == "true" ]; then
   COQPROJECT_HEADER="$COQPROJECT_HEADER
 # Dune compatibility
 -R _build/default/theories HoTT
--Q _build/default/contrib HoTT.Contrib
--Q _build/default/test HoTT.Tests
+-Q _build/default/contrib HoTT_Contrib
+-Q _build/default/test HoTT_Tests
 "
 fi
 
diff --git a/test/dune b/test/dune
index 08fb8df7c9..637a4d0c94 100644
--- a/test/dune
+++ b/test/dune
@@ -1,5 +1,5 @@
 (coq.theory
- (name HoTT.Tests)
+ (name HoTT_Tests)
  (theories HoTT))
 
 (include_subdirs qualified)