diff options
| author | Guillaume Melquiond | 2016-07-07 17:54:03 +0200 |
|---|---|---|
| committer | Guillaume Melquiond | 2016-07-07 17:54:03 +0200 |
| commit | 3f64bf1be849d1c4040b4d06a3417abd1a57f7d2 (patch) | |
| tree | 5585aa2daf46c3990906a2faff634b3e309b8602 | |
| 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.
| -rw-r--r-- | toplevel/vernac.ml | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml index 7c4920dfb8..f80aedbf3c 100644 --- a/toplevel/vernac.ml +++ b/toplevel/vernac.ml @@ -199,7 +199,7 @@ let display_cmd_header loc com = str " [" ++ str cmd ++ str "] "); Pp.flush_all () -let rec vernac_com verbose checknav (loc,com) = +let rec vernac_com checknav (loc,com) = let interp = function | VernacLoad (verbosely, fname) -> let fname = Envars.expand_path_macros ~warn:(fun x -> msg_warning (str x)) fname in @@ -223,7 +223,7 @@ let rec vernac_com verbose checknav (loc,com) = | v when !just_parsing -> () - | v -> Stm.interp verbose (loc,v) + | v -> Stm.interp (Flags.is_verbose()) (loc,v) in try checknav loc com; @@ -250,7 +250,7 @@ and read_vernac_file verbosely s = * raised, which means that we raised the end of the file being loaded *) while true do let loc_ast = parse_sentence input in - vernac_com verbosely checknav loc_ast; + vernac_com checknav loc_ast; pp_flush () done with any -> (* whatever the exception *) @@ -275,7 +275,7 @@ let checknav loc ast = if is_deep_navigation_vernac ast then user_error loc "Navigation commands forbidden in nested commands" -let eval_expr loc_ast = vernac_com (Flags.is_verbose()) checknav loc_ast +let eval_expr loc_ast = vernac_com checknav loc_ast (* XML output hooks *) let (f_xml_start_library, xml_start_library) = Hook.make ~default:ignore () |