Jason Gross

Maybe for the options (the things that come after `Set`), you can offer completions for just those things? This seems like an ugly hack, but might have the behavior I...

1. Won't work for me. There are already too many completions for just `Set`, I want to be able to narrow it down more, first. 2. This is why it's...

There are very few cases that I'd want `Set Pr` to give me `Prop`. If I type `Goal Pro`, I should still get `Prop`. Can you instead make it an...

Thanks! This is working well! Can you also do the same thing for `Set Printing` and `Unset Printing`? There are so many options there that the completion is only helpful...

I was not aware. Cool!

Thanks!

Lack of time, mostly

It seems that coqc is no longer able to find its standard library even when the same prefix is passed to `./configure` and `dune install`, if the root of the...

I believe the issue was that I ran `./configure` but not `make dunestrap`

But the config printout should occur before the error checking