The Coq mailing list

[Hugo Herbelin <herbelin AT pauillac.inria.fr>]

  Hi Jasper,

> 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.
>
> How can I make both notations available again?

  Grammar extensions are based on Camlp4 which is LL1. You have to
factor the entries having the same left prefix.

  The command to observe the grammar produced by Notation is

     Print Grammar constr constr.

  In your case, if you simply give

    Notation "a =' b 'in' c" := (myeq c a b).
    Notation "a =' b" := (myeq ? a b).

  then "Print Grammar constr constr" shows

  ...
| "1" RIGHTA
  [ SELF; "='"; constr:lconstr; "in"; NEXT
  | SELF; "='"; NEXT
  ...

which means that the rules are not factorized. This is because, the
default is to put the rules at level 1 with no associativity (hence
the ending NEXT) and to put inner terms at the applicative level
called lconstr and refered to as level 10 (hence the middle
constr:lconstr). To respect the non-associativity of =, what you need
to do is to force b in the notation "a =' b in c" to be at the next
level, which is level 0. Then say

    Notation "a =' b 'in' c" := (myeq c a b) (b at level 0).

and it will work.

  By the way, predicate tends to be put at level 5 in V7.4, hence a
better syntax extension is

    Notation "a =' b 'in' c" := (eq c a b) (at level 5, b at level 4).
    Notation "a =' b" := (eq ? a b) (at level 5, only parsing).

  where "only parsing" means that it is the first notation which will be
used for printing.

  For more informations, look at chapter 10 of the reference
manual. Notice though that the levels should be reorganized in the
next version of Coq, and that the V7.4 is really a transition version
regarding syntax extensions.

  Hope it helped.

  Hugo