diff options
| author | Maxime Dénès | 2017-02-16 09:44:48 +0100 |
|---|---|---|
| committer | Maxime Dénès | 2017-02-16 09:44:48 +0100 |
| commit | bcb634d070519d6e37d9b7d39f12437a7d38f0c2 (patch) | |
| tree | f14702bb8344d82c264966a95f1257d7184df4a7 /tools | |
| parent | ec49fbd7fee9c6ff27f56498a6309d9651b4ef82 (diff) | |
| parent | 888d4be3ea2a45cff416fd8896276cfa8fc00518 (diff) | |
Merge PR#403: Split Vernacular Processing from Toplevel
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 () ] @ |