diff options
author | Matthieu Sozeau <mattam@mattam.org> | 2016-06-02 14:22:51 +0200 |
---|---|---|
committer | Matthieu Sozeau <mattam@mattam.org> | 2016-06-02 14:25:30 +0200 |
commit | 134fb9534d3e9dd4b20721f9c04fee7db217e883 (patch) | |
tree | 38440a35dbcf7c2137e7c6a47625a2056076174f /toplevel | |
parent | 39741ee5b9c5ea1948e2a97e00e362eea6d936d0 (diff) |
coqtop: Add ltac/ to search path.
For Drop for example.
Diffstat (limited to 'toplevel')
-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 e4975fa31..65c5917b7 100644 --- a/toplevel/coqinit.ml +++ b/toplevel/coqinit.ml @@ -127,7 +127,7 @@ let init_ocaml_path () = [ [ "config" ]; [ "dev" ]; [ "lib" ]; [ "kernel" ]; [ "library" ]; [ "engine" ]; [ "pretyping" ]; [ "interp" ]; [ "parsing" ]; [ "proofs" ]; [ "tactics" ]; [ "toplevel" ]; [ "printing" ]; [ "intf" ]; - [ "grammar" ]; [ "ide" ] ] + [ "grammar" ]; [ "ide" ]; [ "ltac" ]; ] let get_compat_version = function | "8.5" -> Flags.Current |