Lysxia
commented
2 years ago 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 https://github.com/PrincetonUniversity/VST/commit/cd020c2027d309e72c4ebdb12522205731fd4062
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 https://github.com/PrincetonUniversity/VST/issues/590, or unsubscribe https://github.com/notifications/unsubscribe-auth/AATGCAJF6WWNQYFAKJKLYULVPIVAJANCNFSM5Y4MUERA. You are receiving this because you were mentioned.Message ID: @.***>
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:
https://github.com/PrincetonUniversity/VST/pull/588/commits/cd020c2027d309e72c4ebdb12522205731fd4062
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 @mansky1