coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Jason -Zhong Sheng- Hu <fdhzs2010 AT hotmail.com>
- To: "coq-club AT inria.fr" <coq-club AT inria.fr>
- Subject: [Coq-Club] Remove rewrite from hintdb
- Date: Mon, 7 Jan 2019 06:05:17 +0000
- Accept-language: en-CA, en-US
- Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=fdhzs2010 AT hotmail.com; spf=Pass smtp.mailfrom=fdhzs2010 AT hotmail.com; spf=Pass smtp.helo=postmaster AT NAM01-BY2-obe.outbound.protection.outlook.com
- Ironport-phdr: 9a23:1LFNBRO2Ws6QI1DPBBMl6mtUPXoX/o7sNwtQ0KIMzox0Iv/5rarrMEGX3/hxlliBBdydt6oUzbKO+4nbGkU4qa6bt34DdJEeHzQksu4x2zIaPcieFEfgJ+TrZSFpVO5LVVti4m3peRMNQJW2aFLduGC94iAPERvjKwV1Ov71GonPhMiryuy+4ZLebxlLiTanfb9+MAi9oBnMuMURnYZsMLs6xAHTontPdeRWxGdoKkyWkh3h+Mq+/4Nt/jpJtf45+MFOTav1f6IjTbxFFzsmKHw65NfqtRbYUwSC4GYXX3gMnRpJBwjF6wz6Xov0vyDnuOdxxDWWMMvrRr0yRD+s7bpkSAXwhSkHKTA37X3XhMJzgq1Hrx2svAZwz5LIbIyPKPZyYr7RcNUHTmRBRMZRUClBD5u4YYQVFOoBOuBYpJTkq1QNrRu+Ag+sBOzywTFVhn/5w6s60+s4HQrb3gIgAs8FvXParNroNKcTUPu1wLfUwTnec/9bwjf96I/UchAku/6MXLZwfdDNxkkoEgPIl1OdopHmMTONzukAvHSX4/BkWO6xkWIrtht9riWhy8s0hInGmIEYxkzB+Ch8w4s4IcC3R1R+bNOkEZZQuSCXOo54Qs88WG5luCM3xaEJtJO4fyUHzoksyQTFZPydaYeI5wruVOaPLjd8g3JoYKqxigq1/0S81+HwT9S531RUoiZcldnDrW4C2wbU6siaVvty5UCh2SuJ1w/O8O1EOVo0la3HK5E/3rEwipsTsUPFHiPsn0X2kbOWdkEj+uiv6OTreKnpppiZN4NsiwH+NLohmtCnDOk3LgQCRWyW9fqm2LH+50H1XbtHguUzkqbDsZDaIcobprS+Aw9Qyosj5QuwDzen0dQDg3ULME9JdA6cgojpPFHOPPX4Au2+g1Soijtk2/fGPrj5DpXXMnfDiKvhfap660NE1AUzyslf64tIBbEFPfL8QVT8tMfYDx88Kwy72fzrCNR71oMEWGKAGLWVMK3IsQzA2uV6aeKLfcoevCv3A/kj/f/ny3Ej0xdJdq6wmJATdXqQH/J8Ikzfb2C60fkbFmJfnAMlS+qizW+CVjhcL02yUqQzo3kbFcryA4vDVJv32OXZ9Ce8AphfZ2QAAVeJRyS7P76YUusBPXrBavRqlSYJAOD4Gt0RkCq2vQq/8IJJa+/d+ykWr5XmjYMn5+rPkBgz8Xp/CMHPijjRHVExpXsBQnoN5I46uVZ0kwzR0a9khvVZEZpY4PYbCl5nZ66Z9PRzDpXJYiyEftqNTwr5EPOPJGloC/gAmZoJaUs7HMi+hBfe2SbsG6USi7GAGJ0z9OTbwmT1IMF+jX3B0ft4gg==
Hi coq-club,
I am wondering is there a way to remove rewrite hints from the hintdb? I tried Remove Hint but I don't think it works. In my use case, I realized that there is one rewrite rule in one case does too much, so I just want to disable this particular rewrite for
one problem.
- [Coq-Club] Remove rewrite from hintdb, Jason -Zhong Sheng- Hu, 01/07/2019
Archive powered by MHonArc 2.6.18.