Tej Chajed

Yes - it seems to work if you type the first 3 characters correctly. At first I thought it was completing all open sections/modules but it actually seems to pick...

Cool, I'll figure out how to do that.

@paldepind sorry for the long delay - would you mind rebasing on top of master? I gave it an attempt but something about `wptp_recv_strong_normal_adequacy` has changed so that `step_fupd2N_wand` doesn't...

I compared Perennial master with upgraded Iris and stdpp, using a recent Coq master build on OCaml 4.12. This is the difference between 4af744ca7efc24b2d0728b16393c782726eee071 and adb17d55a15dfc72bd091e2d209026241bb19bea. Before the build took...

Sure, I'd be happy to move these to coq-community if others would find them useful. I think the best way to use these tricks is for someone reasonably familiar with...

Ah, just noticed that section in the manifesto - this repo is a perfect example. I integrated some things in that FAQ. I think Eddie Kohler's [Naive Coq](https://github.com/readablesystems/cs260r-17/blob/master/naivecoq.md) tutorial from...

Yeah, looks like I could use coqrst with a reset directive after every example, generating a page just like the Coq reference manual. I'll give that a try at some...

I would also like to see this. As @graingert points out, this would be useful even if it only supported getting the grammar from a URL.

This would be great; just to add more data, in POPL 2020, 17 out of the 40 artifacts used Coq.

Hi @chewxy! Thanks for the offer. We have an undergrad (@sharontlin) working on this already so I do want to leave this open for her to work on. In that...