Created
August 28, 2015 22:17
-
-
Save kai-qu/61e405904ce07a7f4ad9 to your computer and use it in GitHub Desktop.
Error in honeDns in DnsAutoUnify.v
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| In nested Ltac calls to "hone_Dns", "finish_planning", | |
| "IndexTactics" (bound to | |
| fun f => | |
| IndexPackage2 | |
| ltac:(fun FindAttributeUses2 BuildEarlyIndex2 BuildLastIndex2 IndexUse2 | |
| createEarlyTerm2 createLastTerm2 IndexUse_dep2 | |
| createEarlyTerm_dep2 createLastTerm_dep2 BuildEarlyBag2 | |
| BuildLastBag2 => | |
| IndexPackage1 | |
| ltac:(fun FindAttributeUses1 BuildEarlyIndex1 BuildLastIndex1 | |
| IndexUse1 createEarlyTerm1 createLastTerm1 IndexUse_dep1 | |
| createEarlyTerm_dep1 createLastTerm_dep1 BuildEarlyBag1 | |
| BuildLastBag1 => | |
| f ltac:(FindAttributeUses1 FindAttributeUses2) | |
| ltac:(CombineCase6 BuildEarlyIndex1 BuildEarlyIndex2) | |
| ltac:(CombineCase5 BuildLastIndex1 BuildLastIndex2) | |
| ltac:(CombineCase5 IndexUse1 IndexUse2) | |
| ltac:(CombineCase10 createEarlyTerm1 createEarlyTerm2) | |
| ltac:(CombineCase7 createLastTerm1 createLastTerm2) | |
| ltac:(CombineCase7 IndexUse_dep1 IndexUse_dep2) | |
| ltac:(CombineCase11 createEarlyTerm_dep1 | |
| createEarlyTerm_dep2) | |
| ltac:(CombineCase8 createLastTerm_dep1 | |
| createLastTerm_dep2) | |
| ltac:(CombineCase6 BuildEarlyBag1 BuildEarlyBag2) | |
| ltac:(CombineCase5 BuildLastBag1 BuildLastBag2)))), | |
| "IndexPackage2" (bound to | |
| fun f => | |
| PackageIndexTactics ltac:EqExpressionAttributeCounter | |
| ltac:(LastCombineCase6 ltac:BuildEarlyEqualityIndex) | |
| ltac:(LastCombineCase5 ltac:BuildLastEqualityIndex) ltac:EqIndexUse | |
| ltac:createEarlyEqualityTerm ltac:createLastEqualityTerm | |
| ltac:EqIndexUse_dep ltac:createEarlyEqualityTerm_dep | |
| ltac:createLastEqualityTerm_dep ltac:BuildEarlyEqualityBag | |
| ltac:BuildLastEqualityBag f), "PackageIndexTactics", | |
| "f" (bound to | |
| fun FindAttributeUses2 BuildEarlyIndex2 BuildLastIndex2 IndexUse2 | |
| createEarlyTerm2 createLastTerm2 IndexUse_dep2 createEarlyTerm_dep2 | |
| createLastTerm_dep2 BuildEarlyBag2 BuildLastBag2 => | |
| IndexPackage1 | |
| ltac:(fun FindAttributeUses1 BuildEarlyIndex1 BuildLastIndex1 IndexUse1 | |
| createEarlyTerm1 createLastTerm1 IndexUse_dep1 | |
| createEarlyTerm_dep1 createLastTerm_dep1 BuildEarlyBag1 | |
| BuildLastBag1 => | |
| f ltac:(FindAttributeUses1 FindAttributeUses2) | |
| ltac:(CombineCase6 BuildEarlyIndex1 BuildEarlyIndex2) | |
| ltac:(CombineCase5 BuildLastIndex1 BuildLastIndex2) | |
| ltac:(CombineCase5 IndexUse1 IndexUse2) | |
| ltac:(CombineCase10 createEarlyTerm1 createEarlyTerm2) | |
| ltac:(CombineCase7 createLastTerm1 createLastTerm2) | |
| ltac:(CombineCase7 IndexUse_dep1 IndexUse_dep2) | |
| ltac:(CombineCase11 createEarlyTerm_dep1 createEarlyTerm_dep2) | |
| ltac:(CombineCase8 createLastTerm_dep1 createLastTerm_dep2) | |
| ltac:(CombineCase6 BuildEarlyBag1 BuildEarlyBag2) | |
| ltac:(CombineCase5 BuildLastBag1 BuildLastBag2))), | |
| "IndexPackage1" (bound to | |
| fun f => | |
| PackageIndexTactics ltac:IsPrefixExpressionAttributeCounter | |
| ltac:BuildEarlyFindPrefixIndex ltac:BuildLastFindPrefixIndex | |
| ltac:PrefixIndexUse ltac:createEarlyPrefixTerm ltac:createLastPrefixTerm | |
| ltac:PrefixIndexUse_dep ltac:createEarlyPrefixTerm_dep | |
| ltac:createLastPrefixTerm_dep ltac:BuildEarlyTrieBag ltac:BuildLastTrieBag | |
| f), "PackageIndexTactics" and "f" (bound to | |
| fun FindAttributeUses1 BuildEarlyIndex1 BuildLastIndex1 IndexUse1 | |
| createEarlyTerm1 createLastTerm1 IndexUse_dep1 createEarlyTerm_dep1 | |
| createLastTerm_dep1 BuildEarlyBag1 BuildLastBag1 => | |
| f ltac:(FindAttributeUses1 FindAttributeUses2) | |
| ltac:(CombineCase6 BuildEarlyIndex1 BuildEarlyIndex2) | |
| ltac:(CombineCase5 BuildLastIndex1 BuildLastIndex2) | |
| ltac:(CombineCase5 IndexUse1 IndexUse2) | |
| ltac:(CombineCase10 createEarlyTerm1 createEarlyTerm2) | |
| ltac:(CombineCase7 createLastTerm1 createLastTerm2) | |
| ltac:(CombineCase7 IndexUse_dep1 IndexUse_dep2) | |
| ltac:(CombineCase11 createEarlyTerm_dep1 createEarlyTerm_dep2) | |
| ltac:(CombineCase8 createLastTerm_dep1 createLastTerm_dep2) | |
| ltac:(CombineCase6 BuildEarlyBag1 BuildEarlyBag2) | |
| ltac:(CombineCase5 BuildLastBag1 BuildLastBag2)), last call failed. | |
| Error: Illegal tactic application. |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment