The Coq mailing list

[Clément Pit--Claudel <clement.pit AT gmail.com>]

Thanks! That's extremely helpful.

On 07/01/2015 11:23 PM, Valentin Robert wrote:
> <call val="Init"><option val="none"/></call>
> <value val="good"><state_id val="1"/></value>
> 
> <call val="Add">
>   <pair>
>     <pair>
>       <string>Theorem t : forall n, 0 + n = 0.</string>
>       <int>0</int>
>     </pair>
>     <pair>
>       <state_id val="1"/>
>       <bool val="false"/>
>     </pair>
>   </pair>
> </call>
> <value val="good"><pair><state_id val="2"/><pair><union 
> val="in_l"><unit/></union><string></string></pair></pair></value>
> 
> <call val="PrintAst"><state_id val="2"/></call>
> <value val="good"><gallina begin="0" end="32"><theorem begin="0" end="32" 
> type="Theorem" name="t"><apply begin="12" end="31"><operator begin="12" 
> end="31" name="forall"/><constant begin="19" end="20" name="n"/><apply 
> begin="22" end="31"><operator begin="22" end="31" name="_ = _"/><apply 
> begin="22" end="27"><operator begin="22" end="27" name="_ + _"/><token 
> begin="22" end="23">0</token><constant begin="26" end="27" 
> name="n"/></apply><token begin="30" 
> end="31">0</token></apply></apply></theorem></gallina></value>
> 
> <call val="Quit"><unit/></call>