From 134fb9534d3e9dd4b20721f9c04fee7db217e883 Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Thu, 2 Jun 2016 14:22:51 +0200 Subject: coqtop: Add ltac/ to search path. For Drop for example. --- 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 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 -- cgit v1.2.3