The current state of
include_subdirs bothers me. I see a couple of issues:
Previously, I suggested the workaround of making
include_subdirs separate for OCaml and Coq. Today, I don't like the idea anymore for the simple reason that coq users shouldn't need to know about this incantation at all.
With this in mind, I propose the following:
include_subdirswill stop affecting coq stanzas
coq.theorywill also read subdirectories by default. This will only affect coq sources
Do you like this simplification?
Indeed it sounds reasonable that we don't need to do include_subdirs for Coq
IMHO, I think we should move towards whatever direction we'd like to be when in
using coq 2.0we break compatiblity with the current system
I guess that keeping the "Haskell style" structure sounds good
To be clear, this isn't a breaking change (as far as I can tell). It would just mean that
(include_subdirs qualified) would be redundant
Last updated: Nov 29 2023 at 04:01 UTC