The Coq mailing list

[Jasper Stein <jasper AT cs.kun.nl>]

Hugo Herbelin wrote:

>   I seize to opportunity to question the relevance of continuing
> supporting Grammar (for constr) in the next versions of Coq knowing
> that a new mechanism for symbolic notations has been developed. The
>
>   However it does not support recursive notations and hence does not
> allow to write a list in a format like << a b c >> or {a;b;c;d}, etc.

I do hope that we can still use the Grammar subsystem for tactics 
though. (I mean "Grammar Tactic Simple_tactic := ..." etc., not just 
Tactic Definition.) Or alternatively that there is another means of 
defining this recursive-like kind of tactics. I mean, I very often use a 
self-defined tactic that takes a variable number of arguments; it acts 
exactly like Apply, which can have the form "Apply lemma" or "Apply 
otherLemma with arg1 arg2 ... argn", n depending on the lemma involved. 
Since I use it >1300 times, it +must+not+ go away!
--

Jasper
--
+++ Out of Cheese error +++ MELON MELON MELON +++ Redo from Start +++