Stream: Coq devs & plugin devs

Topic: coqdep fails on import cats

view this post on Zulip Ali Caglayan (May 10 2022 at 16:35):

@Gaëtan Gilbert 

dune exec -- coqdep test-suite/success/PartialImport.v
*** Error: File "test-suite/success/PartialImport.v",characters 1832-1833:
           Syntax error

Looks like the coqdep lexer needs to handle import cats better.

view this post on Zulip Gaëtan Gilbert (May 10 2022 at 16:37):

make an issue

view this post on Zulip Ali Caglayan (May 10 2022 at 16:42):

https://github.com/coq/coq/issues/16010

Last updated: Dec 07 2023 at 18:01 UTC