The Coq mailing list

["fengsheng" <fsheng1990 AT 163.com>]

Hello everyone:
     I'm studying the [Software Foundations] written by Benjamin C. Pierce.
I was confused when I was reading the chapter [ImpParser,Lexing and parsing in
coq].
Eval compute in parse "
    x := 3;
    IF x <= 1
       THEN y := 3
       ELSE z := 4
    END".
(*
====>
    SomeE
         (Id 0 ::= ANum 2;
          IFB BLe (AId (Id 0)) (ANum 1) THEN Id 2 ::= ANum 3
          ELSE Id 3 ::= ANum 4 FI, [])
*)
The Id 2 is followed by the Id 0.But there is no other variable between
them.Where is the Id 1?Later I found every time the expression was used, the
symtable would be called and the index plus one.Is it the reason about the
problem? How to solve this bug?

Here is a link of my problem.
http://www.cis.upenn.edu/~bcpierce/sf/ImpParser.html