CompCert
CompCert copied to clipboard
Some dual-licensed code, such as PrintCsyntax, depends on NCL-only sources
Since PrintCsyntax is dual-licensed, I expected it could be used in a GPL project. But according to tools/modorder .depend.extr cfrontend/PrintCsyntax.cmx (using opam coq-compcert v3.8 package, in case it matters), it indirectly depends on some NCL-only source files.
The problem comes (at least in part) from its dependency on cfrontend/C2C.ml which is dual-licensed but directly depends on NCL-only sources such as cfrontend/Initializers.v, driver/Configuration.ml, etc.