The extra toposort reintroduced in #163 is actually unnecessary. The fact that it "works" is a fluke. The reordering problem in CoreFVs that Eric ran into was due to the rewrite rule using an unqualified name, which hs-to-coq doesn't know how to resolve so it can't see the dependency. This PR fixes that.
Removing the unnecessary toposort would break more stuff because order rules are incomplete, so I haven't done that yet.
The extra toposort reintroduced in #163 is actually unnecessary. The fact that it "works" is a fluke. The reordering problem in
CoreFVsthat Eric ran into was due to the rewrite rule using an unqualified name, which hs-to-coq doesn't know how to resolve so it can't see the dependency. This PR fixes that.Removing the unnecessary toposort would break more stuff because
orderrules are incomplete, so I haven't done that yet.