Wierd error in Equiv.v

[Daniel Haskin]

I get the following error when in the Himp module in Equiv.v when the compiler tries to compile the 'new' definition of ceval:
The term "SKIP" has type "com" while it is expected to have type "Imp.com".
I do not get why this happens. I even checked out a fresh 'sf' book and it still happens, even on a fresh copy of Equiv.v/Imp.v.

What do I do now?

HELP!

[Daniel Haskin]

I think I found the problem.

Consider the offending line:
| E_Skip : forall st : state, SKIP / st || st

I have to use coq 8.4 for OS reasons. The error message complains that it wants the 'new' com, not the old, but that this statement yiels 'Imp.com'. This must mean that the notation 'a / b || c' is still registering as 'Imp.com'. Removing the notation:
| E_Skip : forall st : state, ceval SKIP st st
I find no more problems.

I guess 'Reserved Notation' doesn't work so well in 8.4 .

[Jay McCarthy]

That's really strange. I don't see the same problem on my side with coqc. I wonder if the IDE is slightly different. In any case, I'm glad you found it. 

--
You received this message because you are subscribed to the Google Groups "byu-cs-430-winter-2013" group.
To unsubscribe from this group and stop receiving emails from it, send an email to byu-cs-430-winter...@googlegroups.com.
For more options, visit https://groups.google.com/groups/opt_out.
 
 

--
Jay McCarthy <j...@cs.byu.edu>
Assistant Professor / Brigham Young University
http://faculty.cs.byu.edu/~jay

"The glory of God is Intelligence" - D&C 93