From 569cf23a28c344fe32bd4e9712a4e2028c350de2 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Wed, 1 Apr 2015 13:52:56 +0200 Subject: Fixing inclusion of user contrib directory in the loadpath. --- toplevel/coqinit.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'toplevel') diff --git a/toplevel/coqinit.ml b/toplevel/coqinit.ml index 03074ced7..5222d8774 100644 --- a/toplevel/coqinit.ml +++ b/toplevel/coqinit.ml @@ -72,7 +72,7 @@ let add_stdlib_path ~unix_path ~coq_root ~with_ml = Mltop.add_rec_ml_dir unix_path let add_userlib_path ~unix_path = - Mltop.add_path ~unix_path ~coq_root:Nameops.default_root_prefix ~implicit:false; + Mltop.add_rec_path ~unix_path ~coq_root:Nameops.default_root_prefix ~implicit:false; Mltop.add_rec_ml_dir unix_path (* Options -I, -I-as, and -R of the command line *) -- cgit v1.2.3