chore: HoTT.Tests -> HoTT_Tests, HoTT.Contrib -> HoTT_Contrib

This fixes issues #2313 and #2285 by avoiding ambiguous module paths
like HoTT.Contrib.X which could conflict with HoTT.X.


Signed-off-by: Ali Caglayan <[email protected]>

Author: Alizter

contrib/dune

@@ -1,4 +1,4 @@
 (coq.theory
- (name HoTT.Contrib)
+ (name HoTT_Contrib)
  (package coq-hott)
  (theories HoTT))

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
 

test/dune

@@ -1,5 +1,5 @@
 (coq.theory
- (name HoTT.Tests)
+ (name HoTT_Tests)
  (theories HoTT))
 
 (include_subdirs qualified)