Skip to content

Disable Implicit Generalization for Typeclass Arguments

Simon Spies requested to merge simon/typeclass-implicit-arguments into master

This MR removes the implicit generalization of many type class arguments in the Iris code base. Concretely, it adds ! to many type class arguments, which prevents Coq from adding "invisible" arguments to the context. This PR should have no observable effect on other parts of Iris or reverse dependencies, but it should make the code more robust to future changes (e.g., the addition of arguments to some of these type classes).

Merge request reports