The Coq mailing list

[Dan Colish <dcolish AT cecs.pdx.edu>]

On May 14, 2010, at 3:27 AM, Hugo Herbelin wrote:

> 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.
> 


I believe your notation is incorrect. It should be 
[[
Notation "'IFB' e1 'THEN' e2 'ELSE' e3 'FI'" := 
  (CIf e1 e2 e3) (at level 80, right associativity).
]]

The example you provided uses [IF b1 THEN c1 ELSE c2], but it should be the 
notation above or [IFB b1 THEN c1 ELSE c2]. If you are still having conflicts 
double check the imports for that chapter.

--Dan