coq-club AT inria.fr

Subject: The Coq mailing list

List archive

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

From: Théo Zimmermann <theo.zimmi AT gmail.com>
To: Coq Club <coq-club AT inria.fr>
Subject: Re: [Coq-Club] tampering with discharged assumptions of "in" tactical
Date: Tue, 18 Jun 2019 08:54:23 +0200
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=theo.zimmi AT gmail.com; spf=Pass smtp.mailfrom=theo.zimmi AT gmail.com; spf=None smtp.helo=postmaster AT mail-ua1-f42.google.com
Ironport-phdr: 9a23:yqKjKhK/KaJKL0MuedmcpTZWNBhigK39O0sv0rFitYgRLPXxwZ3uMQTl6Ol3ixeRBMOHsqsC0rSG+Pm5ACQp2tWoiDg6aptCVhsI2409vjcLJ4q7M3D9N+PgdCcgHc5PBxdP9nC/NlVJSo6lPwWB6nK94iQPFRrhKAF7Ovr6GpLIj8Swyuu+54Dfbx9HiTagfL9+Ngi6oATSu8UZnIduN7s9wQbVr3VVfOhb2XlmLk+JkRbm4cew8p9j8yBOtP8k6sVNT6b0cbkmQLJBFDgpPHw768PttRnYUAuA/WAcXXkMkhpJGAfK8hf3VYrsvyTgt+p93C6aPdDqTb0xRD+v4btnRAPuhSwaLDMy7n3ZhdJsg6JauBKhpgJww4jIYIGOKfFyerrRcc4GSWZdW8pcUTFKDIGhYIsVF+cOMuhYoIv9qVUArhWwGBeiC//0xzBSmnP7x7c33/g9HQzE2gErAtIAsG7TrNXwLKocT+C1y7PPzTrbbPxW2DL96I3WfRA7pPGDR7RwcczMwkQoCwPFjkufqYv/MzKU1+QNtm2b7+t7WOKgjm4osQBxojy1ysgwjYnJg5sYx1bZ/it62IY4PcO0RFJ/bNK+E5ZdtzuWO5VoTs88WW1ltzg2x7sbspChZicK0o4oxxvHZvyHbYeI5hXjWf6UIThihXJlfKuzhwuo/kS90+H8WMa53EhQoipKldnMsX8N1xjN5cSdVvR9+UKh1S6O1wDV9O5EPVg5mbTHJ5Ml2LI9lZoevV7dEiPohkn6lqCbels89uit8evnY7HmppGGN49zjwHzKrgumsyhDuQ/KAQPXmmb+eG51L3i5kD5T7BKgec3kqndqpzVOcMbpquhDw9Pzokj8wq/Dyuh0NkAgXYHK0tFdAubgIjtJlHBO+v1Dey/glSpiDdk3erKPrznApXXL3jMiq3tfbhn6x0U9A1m5tdGr7lQF7tJdPn0Qwr6sMHSJh4/KQ29hej9XoZTzIQbDF6Pg6iuAqLXtFKS4+spJaHYeI8Yv3DvKv0g5tbhiHY4nRkWeqz/jshfU2yxAvkzexbRWnHrmNpUVD5S5lNiHtyvs0WLVHtoX1j3R7g1v2hpB4evDIOFTYeo0uTYjXWLW6ZOb2UDMWiiVHLhdoGKQfAJMXvALcpokzhCXr+kGdZ4iEOe8TTiwr8iFdL6vy0VsZW5iYpw7uzX0Aw7rHl6U57b3GaKQGV52GgPQm1u0Q==

I don't know what this message means but please open an issue about it: error messages should be documented and appear in the corresponding index of the manual.

All I can say is that this looks like an error message of the SSReflect's rewrite tactic, which seems weird given the syntax you gave.

Le mar. 18 juin 2019 à 07:31, Jeremy Dawson <Jeremy.Dawson AT anu.edu.au> a écrit :

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