You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
As of Coq 8.14 this has become more pressing due to our reliance on Inductive.expand_case in Sexpr.constr2s, which crashes because the recorded proof states are not properly discharged.
That is, can we do more to discharge definitions into recorded proof states? It is not clear whether or not this is actually desirable.
The text was updated successfully, but these errors were encountered: