The Coq mailing list

[anoun AT labri.fr]

Hi everybody,
We need to use the internal representation of a Coq file.
We tried to use the function parse_vernac but unfortunately it doesn't give us
the appropriate result .

Example:

Coq>Drop.
# #use "base_include";;
......
#parse_vernac " forall (A:Prop), A->A."

---> the result is an exception, whereas we expected to find a CCI term of the
form Prod(....).

Thanks a lot for helping us.
Regards,
Houda & Yann


----------------------------------------------------------------
This message was sent using IMP, the Internet Messaging Program.