diff options
| author | Hugo Herbelin | 2015-07-06 23:37:42 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2015-07-07 00:16:14 +0200 |
| commit | 2a28c677c3c205ff453b7b5903e4c22f4de2649b (patch) | |
| tree | 67f6148c95dba2169b5558b05961e44acd566f9b | |
| parent | 2face8d77628ded64f7d0a824f4b377694b9d7fd (diff) | |
Fixing "Load" without "Verbose" in coqtop, after vernac_com lost its
verbose flag.
| -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 bc8aa2fffa..966b952016 100644 --- a/toplevel/vernac.ml +++ b/toplevel/vernac.ml @@ -215,7 +215,7 @@ let display_cmd_header loc com = str " [" ++ str cmd ++ str "] "); Pp.flush_all () -let rec vernac_com checknav (loc,com) = +let rec vernac_com verbose checknav (loc,com) = let interp = function | VernacLoad (verbosely, fname) -> let fname = Envars.expand_path_macros ~warn:(fun x -> msg_warning (str x)) fname in @@ -241,7 +241,7 @@ let rec vernac_com checknav (loc,com) = | v when !just_parsing -> () - | v -> Stm.interp (Flags.is_verbose()) (loc,v) + | v -> Stm.interp verbose (loc,v) in try checknav loc com; @@ -268,7 +268,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 checknav loc_ast; + vernac_com verbosely checknav loc_ast; pp_flush () done with any -> (* whatever the exception *) @@ -293,7 +293,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 checknav loc_ast +let eval_expr loc_ast = vernac_com (Flags.is_verbose()) checknav loc_ast (* Load a vernac file. Errors are annotated with file and location *) let load_vernac verb file = |