Renaming HoTT.Tests and maybe HoTT.Contrib

[jdchristensen]

Currently we often use the same path names in the test folder as in the theories folder, which means that From HoTT Require Import Foo.Bar. is ambiguous. As long as Foo.Bar is the full name, Coq prefers to get this from HoTT (i.e. theories) than from HoTT.Tests (i.e. test), but this is not clear to the reader.

So maybe it would be a good idea to rename HoTT.Tests to something like HoTT_Tests?

(We could consider something similar for contrib, but I don't think we have conflicts there, and this could break external users' code.)

This would be done by changing the -Q line in the _CoqProject file. Ali also points out that we will have to also update the dune files' coq.theory's (name) field.

See #2283 for related discussion.

[jdchristensen]

Here are some examples:

test/Algebra/Groups/Group.v   theories/Algebra/Groups/Group.v
test/Pointed/Core.v           theories/Pointed/Core.v
test/WildCat/Opposite.v       theories/WildCat/Opposite.v