Dune support

[Alizter]

You should be able to build this using Dune with something like:

dune

(coq.theory
 (name CentralTypes) ; can be changed
 (theories HoTT)
 (mode vo) ; no native
 (stdlib no) ; not stldlib
 (flags -noinit -indices-matter))

and a dune-project file like:

(lang dune 3.7)
(using coq 0.7)

Then you can simply drop this project into Coq-HoTT and it will build together, or alternatively have them both in a directory with a dune-workspace file containing (lang dune 3.7).

Soon Dune 3.8 will be released and it will mean you can install the HoTT library using opam and build this repo directly. For now you can build them together.

[jarlg]

Thanks! This is good to know, especially that Dune 3.8 will make things more convenient. I might add info about it to the README after its out and I've tested it. (And I guess maybe we might want to add similar info to the Coq-HoTT build instructions.)