The Coq mailing list

[Benjamin Pierce <bcpierce AT cis.upenn.edu>]

>> I have another problem with Imp.v, which is also related to
>> "Notation". The following inductive predicate should
>> be entirely defined using programming language notation,
>> but Coq is unable to parse "IF b1 THEN c1 ELSE c2" here.
>> Printing is OK. The conflict is with IF... then... else
>> from Init/Logic.v which seems to prevent a different use of IF.
> 
> In Imp.v, I only see a notation "IFB b1 THEN c1 ELSE c2". Did you try
> using this one?
> 
>> Any clue? Is there a convenient solution with scopes?
> 
> If notations had been exactly the same (same keywords, same case),
> scopes could have been used to modify the interpretations.

By the way, since this conversation started with the way we use notations in 
the Software Foundations materials, I should say that we're very open to 
better suggestions about how to use notations so they (look nicer and/or) 
don't conflict with standard library stuff...

    - Benjamin