The Coq mailing list

[Matthieu Sozeau <mattam AT mattam.org>]

Yes you can trick the system by doing a Check foo in a hidden section IIRC. The new coqdoc could do that much more sanely.

On Wednesday, January 22, 2014, Pierre Boutillier <pierre.boutillier AT pps.univ-paris-diderot.fr> wrote:
> Le mardi 21 janvier 2014 à 13:23 -0500, Abhishek Anand a écrit :
>
> > Does coqdoc already invoke coqtop?
> The distributed coqdoc does not.
> this one : https://github.com/thethirdman/coq/compare/coqdoc-dev does.
> It should be in v8.5...
>
>
> All the best,
> Pierre B.


-- 
-- Matthieu