Iris merge requestshttps://gitlab.rts.mpi-sws.org/iris/iris/-/merge_requests2021-05-27T21:38:14Zhttps://gitlab.rts.mpi-sws.org/iris/iris/-/merge_requests/689Change the tactic for resolving Equiv and Dist from an Ofe definition.2021-05-27T21:38:14ZJacques-Henri JourdanChange the tactic for resolving Equiv and Dist from an Ofe definition.The previous hints used eapply. The new hint now use refine. These two
tactic use a different unification algorithm, which result in
different behavior with respect to canonical structures.
The refine tactic is followed by shelving all ...The previous hints used eapply. The new hint now use refine. These two
tactic use a different unification algorithm, which result in
different behavior with respect to canonical structures.
The refine tactic is followed by shelving all the remaining goals,
which correspond actually to existential variables.
In particular, in RustHornBelt, the version using apply is unable to
find the canonical structure of heterogeneous lists.
This change should be mostly backward compatible. However, it makes type-checking of `option_fmap_mono` diverge because different resolution order choices are made by this other tactic. Note that the statement of that lemma was too weakly annotated since it did not even mention `option`. Adding this annotation fixes the issue, and I don't think it is a bad thing to add that annotation.