The Coq mailing list

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

Hello all,

Sadly, in Coq 7.4 the Grammar commands have been discontinued. This 
brings a lot of trouble for at least me, but maybe you can help 
alleviate some!

My present problem is as follows: in Coq 7.3 I could define the notations
 a =' b       meaning (Equal a b)
 a =' b in c  meaning (Equal 1!c a b)
where Equal is some binary relation with one implicit and two explicit 
commands.

Nowadays if I say
Notation "a =' b" := ...
Notation "a =' b 'in' c" := ...
(in this or reverse order) then Coq will allow me only to use the lastly 
defined one.

I can also use the original (coq 7.3.1) expressions defining my Grammar 
rules, but in this case, too, only the last expression seems to be 
accepted in scripts.

How can I make both notations available again?



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