The Coq mailing list

[Michael George <mdgeorge AT cs.cornell.edu>]

Hi,

Is it possible to generate a document containing just the comments and type signatures for my coq code?  I see that I can specify -l to omit proofs, but my definitions are just as unhelpful for documentation.  I have a bunch of definitions like:

(** foo computes the frobnification of bar.  The frobnification is computed by ... *)
Definition foo (x:bar) : baz := match x with
 | case 1
 | case 2
 | ...
 | lots of cases
end.

(** qux evaluates to the most important bar. *)
Fixpoint qux (...) := ...

(** There's really only one bar and it's qux. *)
Lemma important_face: forall x : bar, foo(x) = qux.

and it would be very helpful to get something like the javadoc output:

Definition foo (x:bar) : bar	foo computes the frobnification of x.
Definition qux : bar	qux evaluates to the most important bar.
Lemma important_fact: forall x : bar, foo(x) = qux	There's really only one bar and it's qux.

With the fuller documentation (but still no definitions) below.  Is there any way to coerce coqdoc into giving me just this summary information, or is there another tool that would do the trick?

As an aside, I think the online documentation for the standard libraries would be much more useful in this kind of format.

Thanks,

--Mike