Ssreflect Users Discussion List

[Georges Gonthier <>]

  This is because 'of' is a keyword in ssreflect. Keywords are set by the 
ssreflect.v file, so you should be fine if you only require (not import) 
ssreflect -- which will unfortunately prevent you from using the ssreflect 
rewrite tactic.
  The problem comes from a longstanding design flaw in the Coq lexical 
engine, which segregates keywords from reserved identifiers, and makes it 
impossible for ML plugins to actually add new keywords. Hence, the "of" in 
[Next Obligation of] is a reserved identifier, not a keyword, and cannot be 
matched with the literal keyword "of". The ssreflect plugin tries to mitigate 
this issue by backpatching (with Obj.magic, sic) all the standard parsing 
entries of the Coq grammar to let them recognize the ssreflect keywords (of 
or by), but it doesn't handle the Program grammar (I'm not even sure it could 
access it).

  Best,

Georges


-----Original Message-----
From:  [] 
Sent: 22 January 2010 13:26
To: 
Subject: cannot use [Next Obligation of]

Hello,

It seems that I cannot use the [Next Obligation of] tactic when ssreflect is
imported.
I hit an syntax error. 

Best,
Keiko