coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Ltac, divergence

From: Marthe Bonamy <marthe.bonamy AT ens-lyon.fr>
To: Gert Smolka <smolka AT ps.uni-saarland.de>
Cc: coq-club AT inria.fr
Subject: Re: [Coq-Club] Ltac, divergence
Date: Thu, 22 Jul 2010 13:26:43 +0200
Domainkey-signature: a=rsa-sha1; c=nofws; d=gmail.com; s=gamma; h=mime-version:sender:in-reply-to:references:date :x-google-sender-auth:message-id:subject:from:to:cc:content-type; b=kPw/0AA4Yhu03swx9igqBWNvLjGv97xk4NfszQwMfForPdIe7dN5p0NH6xslmx87C7 ecBWuJgcN615h9mac7vDa6LOq4IA+wzlmv7tjeM2BZ1TGRgPPLAWlyA7ZLsO7NrEAjjD uEIuXH+65lQLBp/p5zGzgZgn3pJQ5jOMXRfzw=

Hi Gert,

I have no clue for 1, but for 2, a naive approach is to use Tactic Notation.

Ltac test2 := simpl.

Tactic Notation "test" := test2.

And then everything is fine, or so it seems.

Hope this helps.

Marthe

On 22 July 2010 11:31, Gert Smolka <smolka AT ps.uni-saarland.de> wrote:

We have defined some tactics to simulate tableaux for teaching. �Sometimes the students supply too many arguments and the Ltac interpreter does not terminate. �Here is a simplified example:

Ltac test := simpl.
Goal True. test H.

1. Where does the non-termination come from?
2. How can I define test such that the extra argument results in failure with an error message?

Thanks,
Gert

[Coq-Club] Ltac, divergence, Gert Smolka
- Re: [Coq-Club] Ltac, divergence, Marthe Bonamy
- Re: [Coq-Club] Ltac, divergence, Jean-Marie Madiot