The source project of this merge request has been removed.
Adapt w.r.t. coq/coq#12512.
This removes the reliance on auto using clauses being arbitrary terms. In theory, should be backwards compatible.
Edited by Ralf Jung
This removes the reliance on auto using clauses being arbitrary terms. In theory, should be backwards compatible.