I have two projects - DynSem (A) - and - DynSem2Coq (B). B depends on and extends A. I’ve enabled completions in A by importing the generated completion.str file. This does not cause any problems. However, building B fails now because it tries to import the completion.str in the B project. However nothing in B imports anything in completions. It appears that somehow paths get confused.

Submitted by Vlad Vergu on 18 April 2017 at 09:44

The dynsem2coq extension does actually import completion.str via the following import chain: dynsem2coq > main > ds2ds/- > ds > completion/completion.

The completion file in turn imports a whole bunch of pretty-printing files, which imported a bunch of half-defined pretty-printing strategies from the NaBL2 library, which caused an error. Hendrik fixed these half-defined pretty-printing strategies.

Also, ds2ds should probably not import ds to prevent a lot of imports from dynsem2coq into dynsem.