diff options
| author |  letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2007-10-21 13:41:53 +0000 |
|---|---|---|
| committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2007-10-21 13:41:53 +0000 |
| commit | 1d6a9cd4ac13b69d1aa5b06f7046685f2fe400ba (patch) | |
| tree | bd3b2db94703cbbf7e67bb18493bcddd130e5ab3 /tools/coqdoc/output.ml | |
| parent | f67216f5fd47881a181dc32e7d67b4210dacf54e (diff) | |
An error message instead of an empty extraction when the monolithic
extraction is given the name of a .v Module.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10245 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'tools/coqdoc/output.ml')
0 files changed, 0 insertions, 0 deletions