GitLab

The current encoding of STS's has a bad reputation. On several occurances it has happened that newcomers use them and are then told not to, as they are "very painful to use in Coq, and we never actually use them in practice".

Whether this is inherent to the abstraction or if its the current iteration of the encoding is to be figured out. Going forward we should do either of the following:

• Include a disclaimer discouraging people from using them
• Remove the encoding from the repository
• Update the implementation to be more user-friendly

I suggest doing either of the first two short-term and then possibly look into the third long-term. It might make most sense to do the disclaimer to maintain correspondence with the formal documentation.