This removes the reliance on auto using clauses being arbitrary terms. In theory, should be backwards compatible.
https://github.com/coq/coq/pull/12512