coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] ltac error?

From: Jeremy Dawson <Jeremy.Dawson AT anu.edu.au>
To: "coq-club AT inria.fr" <coq-club AT inria.fr>
Subject: [Coq-Club] ltac error?
Date: Sun, 7 Apr 2019 15:17:54 +0000
Accept-language: en-US
Authentication-results: mail3-smtp-sop.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-SY3-obe.outbound.protection.outlook.com
Ironport-phdr: 9a23:cEl7PRVZ9kyy2v3k/RfvR2mgnpTV8LGtZVwlr6E/grcLSJyIuqrYbRWCt8tkgFKBZ4jH8fUM07OQ7/m5HzVZqsbd+DBaKdoQDkdD0Z1X1yUbQ+e9QXXhK/DrayFoVO9jb3RCu0+BDE5OBczlbEfTqHDhpRQbGxH4KBYnbr+tQt2agMu4zf299IPOaAtUmjW9falyLBKrpgnNq8Uam4RvJrssxhfTv3dEZutayGBnKFmOmxrw+tq88IRs/ihNp/4t7dJMXbn/c68lUbFWETMqPnwv6sb2rxfDVwyP5nUdUmUSjBVFBhXO4Q/5UJnsrCb0r/Jx1yaGM8L4S7A0Qimi4LxwSBD0kicHNiU2/3/Rh8dtka9UuhOhpxh4w47JfIGYMed1c63Bcd8GQ2dKQ8BcXDFDDIyhdYsCF+oPM/hFoYnhqVUArhq+ChWjCuzg0TJImmT50Lcm3+g9DQ3L3gotFM8OvnTOq9X1Mb8fX+Srw6nS0zrDavNX0irz5ofSfBEhuvaMXbRtesfWzUcgCRnFgUuVqY3lJT+b2P4CsmaA7+pnU+KikHQoqwdsojS12Mgjl5TJipgPxVDZ7Ch0xps+K96gSENjbtOoDIFcuzyGO4Z0WM8uXm9ltSQgxrEbpZK3YTAGxIk5yxLDcfCKcIuF7gj+WOuTPzt0nmxpdb2+ihqq/0iv1O7xWtWx3VtPridIkcXAu3MI2hDO6MWKReZx80Kl1DaB2A3e6+RJLV0qmaffKZMsxKM7mIAJvkTZBCD2nV37jK+IeUUg/eil8/jqbbv7qJOAKoN4kxzwPaYgl8CmBuQ3KRYBU3Kc+eShyL3s5kr5QKhMjvIriKXZqIraJcMHpqGnHwBVzocj6xG5Dzu819QYgGUHLFZCeBKAjIjlIU3BIPf9DfunglSslilkx+zeM7DuHpnBNGXPnKvjcLpn9kJRxgg+wcpC655IF70NOPfzVVXwtNzcAB85KQu0w+P/Bdt5yIweQ3yAAqqZMa/Iv1GH/OwuI/KLZI8TozvyMf4l5+P0gXAnhFAdYLOl0oEKaHygBPRpP12ZYWbwgtcGCWoFog0+TPXzhFKeVT5Tem29Urkn5jA7DYKmFZ3MSpqsgLyHxie7H4dZanpIClCWQj/UcNDOUPAVLSmWP8VJkzoeVLHnRZVrnUWlsxa/wL56JMLV/DcZvNTtzo4myffUkEQQ+CZ5CtXV/2iSVGZy1jcqSiU72bE5jUVi0VCF+aF+nrpVGcEV7u4fAVRyDoLV0+EvU4O6YQnGZNrcEA/3EOXjOik4S5cK+/FLZk98H9u4iRWahXijBaJTmrCWQpUpoPuFgyrBYv1lwnOD75EPykE8S5IVZ2Sgm+hy+xWVDpObyxzExZbvTrwV2Wv2zEnGzWeKux0HAidNav2cGEsuPQ7Rp9m/4V7eRbizD7hhKhFG1cOJNqpNbJvukElCQ/Dgft/ZZjDolg==

Hi,

I have an Ltac "program" as follows:

Ltac nsgen drs nsr rs c sppc q qin acm inps0 at1 at2 :=
...
at1 ;
...
at2 ;
...

Calling it as follows failed:
nsgen drs nsr rs pp sppc q qin acm inps0 (rewrite app_assoc)
(rewrite app_assoc).
with the message Error: The reference rewrite was not found
in the current environment.
but it succeeded, after defining
Ltac rwapas := rewrite app_assoc.
as follows
nsgen drs nsr rs pp sppc q qin acm inps0 rwapas rwapas.

Then I tried
Ltac rw3 pp1 := rewrite app_assoc ; rewrite (app_assoc _ pp1).
and calling it as
nsgen drs nsr rs c sppc q qin acm inps0 (rw3 pp1) rwmb.
failed with the message
Error: The reference rw3 was not found in the current environment.

What am I doing wrong here?

Thanks

Jeremy

[Coq-Club] ltac error?, Jeremy Dawson, 04/07/2019
- Re: [Coq-Club] ltac error?, Jason -Zhong Sheng- Hu, 04/07/2019