Julin S (Sep 11 2022 at 16:16): Julin S (Sep 11 2022 at 16:16):Thanks! Removing those comments made it work.
But what were the non-ASCII in those comments? I couldn't spot them.
For example, in the first line:
# Avoid module name puns, as it confuses Coq’s code extraction
Which character is non-ASCII?
Karl Palmskog (Sep 11 2022 at 16:16):the ’
Julin S (Sep 11 2022 at 16:23):Oh.. got it. Thanks.
Notification Bot (Sep 11 2022 at 16:23):Julin S has marked this topic as resolved.
Last updated: Feb 06 2023 at 05:03 UTC