Matthieu Sozeau

The user woud have written it. Examples like this are in MathClasses

The motivation is to use an observationally equivalent but more efficient version of an operation AFAIR

In that case it was using priorities (even implicitely, as the specific instance has no premise compared to the general one), but this doesn't in itself prevent backtracking.

Maybe there's a more explicit way to specify this indeed.

I don't think we have the infrastructure to do things like this yet. The issues with quoting/unquoting/calling tc inference under context are quite interesting! With the current reorganization of the...

Thanks for the report! Sadly I don't see an easy way to make the package depend on python in opam

Yes it should do the same. It might be reasonable to have a strict mode of unquoting where universes cannot be created as well, ensuring reproducible results

To be clear, it should be the second version used in ‘live-coq’

My bugfix fixes the example of @eponier but probably not the one of @TheoWinterhalter

I didn't try, but maybe others did. It could be that we lack some support somewhere, did you have an example of something you want to quote/unquote?