Language contribution confuses imports
I have two projects - DynSem (A) - and - DynSem2Coq (B). B depends on and extends A. I’ve enabled completions in A by importing the generatedSubmitted by Vlad Vergu on 18 April 2017 at 09:44
completion.strfile. This does not cause any problems. However, building B fails now because it tries to import the
completion.strin the B project. However nothing in B imports anything in completions. It appears that somehow paths get confused.
dynsem2coqextension does actually import
completion.strvia the following import chain:
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.
ds2dsshould probably not import
dsto prevent a lot of imports from dynsem2coq into dynsem.
Log in to post comments