I/O testcases suffer from lack of automatic instantiation using InteractionTrees 5.0
Closed this issue · 1 comments
andrew-appel commented
In the following commit, having updated the InteractionTrees submodule to ITrees version 5.0 (May 2022), things stopped working. The fix was to explicitly instantiate a certain argument everywhere, because Coq is now failing to instantiate it automatically. You can see exactly where, by looking at the line-by-line diffs here:
My question is, what change to ITrees has caused this, and is there a one-line fix I can put somewhere, after Require Import InteractionTrees.whatever, that will get us back to "automatic instantiation mode"?
Lysxia commented
To get the old behavior back:
#[global] Hint Mode ReSum - - - - : typeclass_instances.
…On 2022-06-15 3:27 PM, Andrew Appel wrote:
In the following commit, having updated the InteractionTrees submodule
to ITrees version 5.0 (May 2022), things stopped working. The fix was to
explicitly instantiate a certain argument everywhere, because Coq is now
failing to instantiate it automatically. You can see exactly where, by
looking at the line-by-line diffs here:
cd020c2
<cd020c2>
My question is, what change to ITrees has caused this, and is there a
one-line fix I can put somewhere, after |Require Import
InteractionTrees.whatever|, that will get us back to "automatic
instantiation mode"?
@Lysxia <https://github.com/Lysxia> @mansky1 <https://github.com/mansky1>
—
Reply to this email directly, view it on GitHub
<#590>, or unsubscribe
<https://github.com/notifications/unsubscribe-auth/AATGCAJF6WWNQYFAKJKLYULVPIVAJANCNFSM5Y4MUERA>.
You are receiving this because you were mentioned.Message ID:
***@***.***>