Anton Trunov

Results 79 comments of Anton Trunov

There is also a couple of new warnings connected to this one, e.g. ``` File "./coq/FunProg.v", line 919, characters 0-23: Warning: Casts are ignored in patterns [cast-in-pattern,automation] ``` It's for...

That sounds great! Thanks a lot for the pointers, @ejgallego @cpitclaudel.

> Please keep me posted, I'm very curious to see how that will turn out. Sure. Speaking of schedule, I think I can start working on this in about a...

Thanks for looking into this issue! So, we have a codebase that uses QuickChick to test the implementation of [Scilla](https://scilla-lang.org). We describe a simplified version of Scilla's syntax, write generators,...

> this is more about documenting how one might set up QC tests with dune This would be really really helpful! > This doesn't need the CLI tool, which I...

Hi @olaure01, I'm wondering about your use case for this new feature. Could you please expand a bit on that?

> -arg -w -arg notation-overriden is supported I think it's not supported though, because I tried that and it didn't work with PG (but it works with CoqIDE). ```emacs-lisp M-:...

> Hmm, but you didn't include it in the input to coq--read-options-from-project-file, so I think that's normal oops, you are right :) I re-checked and the hyphen survives :)

@cpitclaudel #393 fixes the problem, I think; I tested it on on a real Coq project ``` -arg "-w -notation-overriden" -arg -w -arg notation-overriden -arg -w -arg -notation-overriden -arg -w...