diff options
Diffstat (limited to 'tools')
| -rw-r--r-- | tools/coq_makefile.ml | 2 | ||||
| -rw-r--r-- | tools/coqmktop.ml | 1 |
2 files changed, 2 insertions, 1 deletions
diff --git a/tools/coq_makefile.ml b/tools/coq_makefile.ml index b7dd5f2a14..624b9ced7d 100644 --- a/tools/coq_makefile.ml +++ b/tools/coq_makefile.ml @@ -51,7 +51,7 @@ let lib_dirs = ["kernel"; "lib"; "library"; "parsing"; "pretyping"; "interp"; "printing"; "intf"; "proofs"; "tactics"; "tools"; "ltacprof"; - "toplevel"; "stm"; "grammar"; "config"; + "vernac"; "stm"; "toplevel"; "grammar"; "config"; "ltac"; "engine"] diff --git a/tools/coqmktop.ml b/tools/coqmktop.ml index eaf938e8ce..645b3665e0 100644 --- a/tools/coqmktop.ml +++ b/tools/coqmktop.ml @@ -75,6 +75,7 @@ let std_includes basedir = let rebase d = match basedir with None -> d | Some base -> base / d in ["-I"; rebase "."; "-I"; rebase "lib"; + "-I"; rebase "vernac"; (* For Mltop *) "-I"; rebase "toplevel"; "-I"; rebase "kernel/byterun"; "-I"; Envars.camlp4lib () ] @ |