The Coq mailing list

[Gert Smolka <smolka AT ps.uni-saarland.de>]

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