Unless Refine Instance Mode is set (I think it's deprecated and going away), Instance foo := <partial term>. Proof. <more stuff>. Defined. is no longer valid, and instead you need to refine with the partial term. Rather than just setting Refine Instance Mode, I've changed the instance declarations over for more forward-compatibility.
Apparently the order in which return match inference is done changed and match got more eager about eliminating impossible branches. This was causing a later destruct to fail. Adding return _ forced a non-dependent return clause, allowing the later destruct to succeed.
gmalecha
commented
4 years ago
Tested
makewith Coq 8.10.0 and 8.9.1. This builds with both of them assuming the version of coq-ext-lib you have is https://github.com/coq-community/coq-ext-lib/pull/76.There were three errors that needed fixing:
Refine Instance Modeis set (I think it's deprecated and going away),Instance foo := <partial term>. Proof. <more stuff>. Defined.is no longer valid, and instead you need torefinewith the partial term. Rather than just settingRefine Instance Mode, I've changed the instance declarations over for more forward-compatibility.matchgot more eager about eliminating impossible branches. This was causing a laterdestructto fail. Addingreturn _forced a non-dependent return clause, allowing the laterdestructto succeed.