Tej Chajed

This is because at least when we initially developed Goose the go/types package didn't help differentiate nil for a slice vs a pointer (it assigned them the same "untyped nil"...

This is not expected, thanks for letting me know! I’ll try to take a look in the next week or so.

I looked into this and it doesn't look like a simple fix. (The only thing I could do right away is trigger an error because the setter doesn't do anything.)...

Any update on this? I'm also not sure how you generated the HTML files.

Thanks for taking a look Emilio! It seems like `let open Sorts` does fix some warnings, but correctly handling `Set` correctly makes the plugin incompatible with Coq v8.8 so it...

I like this, too! In particular it adds a new feature of opaque theorems with explicit bodies using tactics-in-terms (last I checked `Proof with ltac:(foo).` doesn't work, and it's clunky...

More specifically `Set Printing Projections` is happy to print class instances, which doesn't make much sense to me. Would it be easier to avoid the projection printing when the principal...

I just want to mention that I'm using VS Coq in class _and_ with Perennial. It would still be helpful to have a nice way of building dependencies for the...