Skip to Content.
Sympa Menu

coq-club - [Coq-Club] Remove rewrite from hintdb

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Remove rewrite from hintdb


Chronological Thread 
  • 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.

Sincerely Yours,

Jason Hu


  • [Coq-Club] Remove rewrite from hintdb, Jason -Zhong Sheng- Hu, 01/07/2019

Archive powered by MHonArc 2.6.18.

Top of Page