@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.
make an issue
https://github.com/coq/coq/issues/16010
Last updated: Dec 07 2023 at 18:01 UTC