Xia Li-yao

`bound` tracks the context of a term in the types, which changes when going through binders, this seems quite incompatible with the view in `recursion-schemes` of recursive types as fixed-points...

Should the rest of the path still be `$(dir $(shell which coqc))`? That's an absolute path so it doesn't seem right to concatenate it with `$(DESTDIR)`.

OK I was just not familiar with DESTDIR. It's supposed to be a temporary location for staging installs, which is why it's meant to be prepended it to an absolute...

The QCtool CLI utility follows quite a different codepath from the plugin. Sadly this means recent features like dune support (which get added into the plugin first) might need some...

Yeah, what you describe sounds like a good solution! If I understand correctly, the existing vernaculars should be enough (at least for common use cases), and this is more about...

I would wrap `A` in a sigma (`sigT`?). ``` elems [existT A x, existT A y] : G { b : bool & A b } ```

I'm fine with not fixing it if it's not easy. I just wanted to mention it because it seems somewhat common, but I'm not at all fond of that style.

There may be a hack to change the extraction of the part that sets the seed. This feature also seems quite simple to add properly, just nobody has got around...

The inequality `sig.u0 < eq.u0` seems like the worst offender and it comes from VST. Still, there may be some way to remove the `sig.u0 = eq.u0` constraint from our...

I see something different. ```coq Print Universes Subgraph (sig.u0 eq.u0). (* Prop < Set Set < sig.u0 < eq.u0 *) ```