aboutsummaryrefslogtreecommitdiffhomepage
path: root/toplevel/coqtop.ml
diff options
context:
space:
mode:
Diffstat (limited to 'toplevel/coqtop.ml')
-rw-r--r--toplevel/coqtop.ml2
1 files changed, 0 insertions, 2 deletions
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index da63382bf..696ce1282 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -74,11 +74,9 @@ let outputstate () = if !outputstate <> "" then extern_state !outputstate
let set_default_include d = push_include (d,Nameops.default_root_prefix)
let set_include d p =
let p = dirpath_of_string p in
- Library.check_coq_overwriting p;
push_include (d,p)
let set_rec_include d p =
let p = dirpath_of_string p in
- Library.check_coq_overwriting p;
push_rec_include(d,p)
let load_vernacular_list = ref ([] : (string * bool) list)