Skip to content
GitLab

Adapt w.r.t. coq/coq#12512.

Closed Ghost User requested to merge (removed):globref-in-auto-using into master

This removes the reliance on auto using clauses being arbitrary terms. In theory, should be backwards compatible.

https://github.com/coq/coq/pull/12512

Edited by Ralf Jung