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

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)" > $@

contrib/dune

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

dune

@@ -32,10 +32,10 @@
    HoTT
    -Q
    contrib
-   HoTT.Contrib
+   HoTT_Contrib
    -Q
    test
-   HoTT.Tests
+   HoTT_Tests
    %{deps}
    -o)))
 

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)