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.
Since
PrintCsyntaxis dual-licensed, I expected it could be used in a GPL project. But according totools/modorder .depend.extr cfrontend/PrintCsyntax.cmx(using opamcoq-compcertv3.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.mlwhich is dual-licensed but directly depends on NCL-only sources such ascfrontend/Initializers.v,driver/Configuration.ml, etc.