aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--toplevel/coqtop.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index a5673578f5..a97d8748a6 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -106,7 +106,7 @@ let require_prelude () =
let require_list = ref ([] : string list)
let add_require s = require_list := s :: !require_list
let require () =
- if !load_init then require_prelude ();
+ if !load_init then silently require_prelude ();
List.iter (fun s -> Library.require_library_from_file None s (Some false))
(List.rev !require_list)