The Coq mailing list

[Jean-Marie Madiot <madiot AT gmail.com>]

Hi Gert,

You could use a more recent version of coq. Coq 8.3 (mine is
8.3-beta0) handles correctly this kind of use of Ltac by saying:

  Error: Illegal tactic application.

You can either wait for coq 8.3 to be released, which should happen
soon (end of July?), or if it's possible you can deploy on the
computers used by your students a beta version, available here:
http://coq.inria.fr/distrib/V8.3-beta0/files/ ;(however I recommend
using Marthe's notation hack and then waiting for the release)

Jean-Marie

On Thu, Jul 22, 2010 at 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