coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] tampering with discharged assumptions of "in" tactical

From: Robbert Krebbers <mailinglists AT robbertkrebbers.nl>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] tampering with discharged assumptions of "in" tactical
Date: Tue, 18 Jun 2019 09:00:25 +0200
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=mailinglists AT robbertkrebbers.nl; spf=Pass smtp.mailfrom=mailinglists AT robbertkrebbers.nl; spf=None smtp.helo=postmaster AT smtp2.science.ru.nl
Ironport-phdr: 9a23:fhL5fxASPJ7wRUm/Cb1fUyQJP3N1i/DPJgcQr6AfoPdwSPT/pMbcNUDSrc9gkEXOFd2Cra4d0qyP7fCrADVZqb+681k6OKRWUBEEjchE1ycBO+WiTXPBEfjxciYhF95DXlI2t1uyMExSBdqsLwaK+i764jEdAAjwOhRoLerpBIHSk9631+ev8JHPfglEnjWwba5vIBmssAnct8objYR/Jqos1xfCv2dFdflRyW50P1yYggzy5t23/J5t8iRQv+wu+stdWqjkfKo2UKJVAi0+P286+MPkux/DTRCS5nQHSWUZjgBIAwne4x7kWJr6rzb3ufB82CmeOs32UKw0VDG/5KplVBPklCEKPCM//WrKiMJ/kbhbrQq8qRJhzY7aYIKbOvRwcazSf9wVWWVPU91NVyFDGI6wc5cDAuQDMOtesoLzp0EOrRy7BQS0GO3vzSRHiWTo0q0gz+QqDATI3BY+EN0Vq3vbss/1NLwPWu2yyanH1zTDb/dX2Tf754jIdhEhoeqQXbJrasfR004vGBjegVqOs4zlIzCV1v4TvGeA9OVvS/ivi3U9pwF3pjii38EhgZTHiIISz1DL7yR5wIAtKN23SU57fd6kEIZLuC2AK4R2RcYiTmd1syg50r0LoYO3cSYXxJg92hLSafOKf5KV7h/iTuqdPDh1iXJ9dL6iiBu/8VKsx+nzW8WuzVpGsChInsPRun0O2BHe7NWMROFn8Ue7wzmP0hje6uFaLkAwkqrWM4UhwrsslpoLr0jPBDT2l1n3jKCIcEUr5van5/79YrX7vJOcMYt0hhn/MqQohMO/Hfw1PhUAUmSG4+iwyb/u8ELjTLlXj/A6iLTVvZ/aKMgDo662GQ5V0oIt6xalCDem1cwVnXwdI1JEfBKHjo7pO17KIPD5Fve/n0+snSxxx/DBJbLuGYvCLmLfkLfiZ7Zy9VVTxxEtwtBF/JJYELcBIPbrVk/rqNPYFgM5MxCzw+v/FNp90ZoeVXuTDa+dLaPdqkSF5vkvIumJfI8aoizxK/kj5/70jH82g0URfaez3chfVHftFfN/Zk6dfHDEg9EbEG5MsBBtYvbtjQi4VjRZamyuF4Em6zsxBZi9RdPGT4GpgbqO2CagAoZ+fGdMAF2WDXTyeo+OVu0XLiSWdJwy2gcYXKSsHtdynSqlsxX3nuI+c7jkvxYAvJem7+Bbou3ekRZorG5vCtiFiSeWRGB5mGgFASUrmqZ78xQklgWzlJNgivkdLuR9outTW11iZ4TbxeZ3EczxQA/LdNqTUxCgRof+WGBjfpcK29YLJn1FNZCnhxHH0TCtBuVNxaaMDpY56L7fxXX7Lctn0DDA0Pt4gg==

This is may be an instance of bug https://github.com/math-comp/math-comp/issues/16

On 6/18/19 7:30 AM, Jeremy Dawson wrote:

Hi ,

I'm trying to rewrite a hypothesis in doing a proof, using the
rewrite -> tactic, but it fails with the message

Ltac call to "rewrite (ssrrwargs) (ssrclauses)" failed.
tampering with discharged assumptions of "in" tactical

What does this message mean?

Thanks,

Jeremy

[Coq-Club] tampering with discharged assumptions of "in" tactical, Jeremy Dawson, 06/18/2019
- Re: [Coq-Club] tampering with discharged assumptions of "in" tactical, Théo Zimmermann, 06/18/2019
- Re: [Coq-Club] tampering with discharged assumptions of "in" tactical, Robbert Krebbers, 06/18/2019