The Coq mailing list

[Tom Prince <tom.prince AT ualberta.net>]

On Sat, 21 Jan 2012 07:09:16 +0100, Stéphane Glondu 
<steph AT glondu.net>
 wrote:
> Le 19/01/2012 17:29, Beta Ziliani a écrit :
> > In one line: is there a library with every ml module in coq?
> > 
> > In two: I would like to write some unit tests for my plugin. For that, I
> > created a .ml file that opens the plugin module and test some functions
> > inside it. I can compile it ok but now I need to link it with every cmo
> > file in the source code of Coq. Is there another way?
> 
> Doesn't coqmktop suit your needs?

In particular, if you don't want to start the coq toplevel, you can use
the option -no-start. See https://gist.github.com/1343032 for an
example.

  Tom