Typeclasses Dependency Order actually do anything?
Typeclass resolution seems to always try to solve the nondependent typeclass goal first, regardless of how I set this
I think you would need to find a caller that uses split:false, ie unification.ml or rewrite.ml, to see a difference
Why is it set up like that? (And what does
(It's documented at https://coq.inria.fr/refman/addendum/type-classes.html#coq:flag.Typeclasses-Dependency-Order as a general setting for typeclass resolution...)
@Gaëtan Gilbert Do you know how to make https://github.com/coq/coq/issues/16760 work?
Last updated: Jan 29 2023 at 05:03 UTC