diff options
| author |  Guillaume Melquiond <guillaume.melquiond@inria.fr> | 2016-07-07 17:55:00 +0200 |
|---|---|---|
| committer | Guillaume Melquiond <guillaume.melquiond@inria.fr> | 2016-07-07 17:55:00 +0200 |
| commit | 947b30150602ba951efa4717d30d4a380482a963 (patch) | |
| tree | 2bcc5a160d18d58e26f12afccf6bed41194cbc17 /toplevel | |
| parent | 3f64bf1be849d1c4040b4d06a3417abd1a57f7d2 (diff) | |
Prevent "Load" from displaying all the intermediate subgoals.
Note that even "Load Verbose" is not supposed to display them.
Diffstat (limited to 'toplevel')
| -rw-r--r-- | toplevel/vernac.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml index f80aedbf3..1f7b947e9 100644 --- a/toplevel/vernac.ml +++ b/toplevel/vernac.ml @@ -213,7 +213,7 @@ let rec vernac_com checknav (loc,com) = end; begin try - read_vernac_file verbosely f; + Flags.silently (read_vernac_file verbosely) f; restore_translator_coqdoc st; with reraise -> let reraise = Errors.push reraise in |