You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
Since 8.16 coq_makefile extracts META files from _CoqProject and passes them to coqdep via -m, see coq/coq#15220. PG should also extract META files, such that a -m switch can be added to coqdep invocations. Otherwise auto-compilation on files using ML modules will fail, see #724.
Note that the -m switch is only a necessary (but no sufficient) condition to support ML modules in auto-compilation.
The text was updated successfully, but these errors were encountered:
Until this feature is implemented, affected users may workaround by setting coq-compile-extra-coqdep-arguments from PR #735. Note that one needs to use absolute path' there, because coqdep is also invoked on temporary files in /tmp that contain single require lines from the current file. The option needs to be set for all files of a project, so it's probably best to set it via directory variables, eg.,
Since 8.16 coq_makefile extracts META files from _CoqProject and passes them to coqdep via
-m
, see coq/coq#15220. PG should also extract META files, such that a-m
switch can be added to coqdep invocations. Otherwise auto-compilation on files using ML modules will fail, see #724.Note that the
-m
switch is only a necessary (but no sufficient) condition to support ML modules in auto-compilation.The text was updated successfully, but these errors were encountered: