diff options
| author |  Guillaume Melquiond <guillaume.melquiond@inria.fr> | 2016-07-07 17:54:03 +0200 |
|---|---|---|
| committer | Guillaume Melquiond <guillaume.melquiond@inria.fr> | 2016-07-07 17:54:03 +0200 |
| commit | 3f64bf1be849d1c4040b4d06a3417abd1a57f7d2 (patch) | |
| tree | 5585aa2daf46c3990906a2faff634b3e309b8602 /test-suite/bugs/closed/3036.v | |
| parent | 0bbc652fc15e1c27b20d3288205079ff295e21da (diff) | |
Do not display goals in -compile-verbose mode (bug #4841).
The -verbose family of options is only meant to echo sentences as they are
processed. The patch below broke this, while fixing another issue. That
other issue will be fixed in the next commit.
Revert "Fixing "Load" without "Verbose" in coqtop, after vernac_com lost its"
This reverts commit 2a28c677c3c205ff453b7b5903e4c22f4de2649b.
Diffstat (limited to 'test-suite/bugs/closed/3036.v')
0 files changed, 0 insertions, 0 deletions