The Coq mailing list

[marko AT ffri.hr]

Hi,

I had the similar needs and I solved it by redirecting output in some txt
file and then by parsing this txt file.

So, something like this:

coqtop.opt -load-vernac-source your_environment.v > "output.txt"

and then you can parse by some MS-DOS or Windows parser lines which
containe hypotheses you need (everything you can do automaticaly).

Hope this help,

Marko Malikoviæ

> Hi,
>
> We want to filter the output file that coqtop sends to the standard
> output.
> Our goal  is to select some hypotheses in the environment according to
> the fact they contain
> some words.
> Our first problem is to split the output into hypotheses. The carriage
> return seems not sufficient
> since a long hypothesis occupies several lines.
> Is there a location where we can find the syntax of the output ?
> Thanks,
>
>     Jean Duprat
>
> --------------------------------------------------------
> Bug reports: http://logical.futurs.inria.fr/coq-bugs
> Archives: http://pauillac.inria.fr/pipermail/coq-club
>           http://pauillac.inria.fr/bin/wilma/coq-club
> Info: http://pauillac.inria.fr/mailman/listinfo/coq-club
>