coq-club AT inria.fr

Subject: The Coq mailing list

List archive

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

From: Jeremy Dawson <Jeremy.Dawson AT anu.edu.au>
To: "coq-club AT inria.fr" <coq-club AT inria.fr>
Subject: [Coq-Club] tampering with discharged assumptions of "in" tactical
Date: Tue, 18 Jun 2019 05:30:42 +0000
Accept-language: en-US
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=Jeremy.Dawson AT anu.edu.au; spf=Pass smtp.mailfrom=Jeremy.Dawson AT anu.edu.au; spf=Pass smtp.helo=postmaster AT AUS01-ME1-obe.outbound.protection.outlook.com
Ironport-phdr: 9a23:wUI0CB1R1Ue+NlxSsmDT+DRfVm0co7zxezQtwd8ZseIeKvad9pjvdHbS+e9qxAeQG9mCsrQd1bqd4vuocFdDyK7JiGoFfp1IWk1NouQttCtkPvS4D1bmJuXhdS0wEZcKflZk+3amLRodQ56mNBXdrXKo8DEdBAj0OxZrKeTpAI7SiNm82/yv95HJbAhEmSexbalvIBi3rgjduc0bjIV/Iast1xXFpWdFdf5Lzm1yP1KTmBj85sa0/JF99ilbpuws+c1dX6jkZqo0VbNXAigoPGAz/83rqALMTRCT6XsGU2UZiQRHDg7Y5xznRJjxsy/6tu1g2CmGOMD9UL45VSi+46ptVRTljjoMOTwk/2HNksF+jLxVrg+9pxJxwIDUYZ2aOvVxca7GYdMVXnBMUtpNWyBdAI6xaZYEAeobPeZfqonwv18AogWkBQayAePuyiJDiHHs0qw0yOQhFgfG1xEnEtwKrnvUtsv6NKISUOyvwqfH1zvCb+hR2Tf784XHaBYhoeyWUb1ubMXR1FMjGBnYjliJr4HuIjCb1vwVvmWU8+ZsT/+jh3Ilpg1rvzSiyMYhhpPNi48a0lzI6CV0zJovKdGmVEJ2b8SoHIVNuy2GLYd6X80vTmVwtCY01LILuoK3cS0PxZknxxPTdf+Kfo2T7R/sT+mePzJ1iXZqdb2lhxu/9FasxfbnWcav1ltBszBLncPWtn8X0hze8siHReV5/kemwTuCyw7c5PxYLUwpjKbVLJEvzqMpmpoUqkvMADX6mELrjK+KbUok/fWo6+L6bbn8vp+cLYh0ih3gPasyhsy/AOM4Mg4UU2ic5OS8yLnj/Ur+QLVJlPE5jq7ZsJXCKcQaoK62HRNV354s5hqjFTuqzcgUkHsdIF5Ydh+KjpLlNlXBLfzgCPewmVWskDNlx/DcOb3hB43AIHzdn7f7Y7l97k5dxBA9w99F6ZNUEbYBIPToV0DrstzYEwU1PBKpzOb6EtlyzJ4eVXqVAqCFKKPSrUOI5uU3LuaQY48VoS/xJOQh5/7zlnA0gkQdfKms3ZsPcn+0BPVmI0ODYXrtmNgNC2kKvhBtBNDt3ReJVicWbHKvVYo94Cs6AcSoF82LEouqmfmK2DqxNpxQfGFPTF6WRyTGbYKBDtUBci+XM4dNmyMfUr7pH60szxyrpUnWwqV8Kez88ysF85/vyZ58+ruAxlkJ6TVoApHFgCm2RGZukzZQHmNk7OVEuUV4j2y7/+1gmfUBT45a4e4PXwsnc5fBnbQjWoLCHznZd9LMc26IB9CvADU/VNU0moVcakBgXdiuk1bKwnjzWuJHp/mwHJUxt5nk8T3xKsJ6lymU/ZQa1wBjZ+YWcGqsi+h46hTZAJPPnwOBjaG2eK8A3SnLsmCe0W6Ju0IeWwl1A/zI

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