We don't want isgraph_paths, is2graph_paths, or is3graph_paths to be global instances, as then Coq could apply them in situations where we prefer a different wild category structure. But the further instances that require having these ones already applied can safely be global instances, so that's what this PR does.
This allows us to simplify things in the three files that currently use WildCat.Paths: Suspension.v, CoeqUnivProp.v and Matrix.v.
I have checked that the build time is unchanged within the noise.
We don't want
isgraph_paths,is2graph_paths, oris3graph_pathsto be global instances, as then Coq could apply them in situations where we prefer a different wild category structure. But the further instances that require having these ones already applied can safely be global instances, so that's what this PR does.This allows us to simplify things in the three files that currently use WildCat.Paths: Suspension.v, CoeqUnivProp.v and Matrix.v.
I have checked that the build time is unchanged within the noise.