Skip to Content.
Sympa Menu

coq-club - [Coq-Club] recursive Ltac definitions

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] recursive Ltac definitions


chronological Thread 
  • From: Aaron Bohannon <bohannon AT cis.upenn.edu>
  • To: Coq Club <coq-club AT inria.fr>
  • Subject: [Coq-Club] recursive Ltac definitions
  • Date: Wed, 20 Oct 2010 12:48:16 -0400
  • Domainkey-signature: a=rsa-sha1; c=nofws; d=gmail.com; s=gamma; h=mime-version:sender:date:x-google-sender-auth:message-id:subject :from:to:content-type; b=FpPkRWhyvyetbcr7g92JTcF5NMpqFtlHA0d9VjC0Y8mTcX+XMJihuHoXKNrIGw6+X3 BC10Zsoq3MroY0JlM00HohpCx6b3P34jJBjWLZHWzpqH5xE0+FyKLUM4o/k16MR1HRef kWcW/0I3lncgqhlbvYfbECgoPZOvA0kMMUsRI=

Why do the first four definitions succeed while the fifth one fails?
(I have a very hard time imagining I'm the first to discover this...)

Ltac t := t.

Ltac t := t t.

Ltac t u := t u.

Ltac t u := t t u.

Ltac t u := t (t u).
Error: The reference t was not found in the current environment.

 - Aaron



Archive powered by MhonArc 2.6.16.

Top of Page