The Coq mailing list

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

Hi Jean-François,

On Fri, May 14, 2010 at 08:31:54AM +0800, Jean-Francois Monin wrote:
> [Previously: Re: [Coq-Club] record field is "lost" if import is used]
> 
> 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.

> BTW I'm unsure that "IF" in Init/Logic.v is as important as 
> usual connectives ("/\", etc.).

I agree but some existing developments may dependent on it. 

Hugo Herbelin