diff options
| author | Pierre-Marie Pédrot | 2015-04-01 13:52:56 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2015-04-01 13:53:20 +0200 |
| commit | 569cf23a28c344fe32bd4e9712a4e2028c350de2 (patch) | |
| tree | bb54ecebff1cf1a12c4ae7cec0671051a1d9c2af | |
| parent | a297f5cbeb5f76cae593a0778605ce9050e9d1c5 (diff) | |
Fixing inclusion of user contrib directory in the loadpath.
| -rw-r--r-- | toplevel/coqinit.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/toplevel/coqinit.ml b/toplevel/coqinit.ml index 03074ced70..5222d87749 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 *) |