diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-02-16 19:05:45 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-02-17 11:52:38 +0100 |
| commit | b09751b9a1b48541acc9a2daaff9ebc453fc3bf7 (patch) | |
| tree | 211886b6204716d3239f36c9b5d5d616394583e1 /tools | |
| parent | 6d49de4f2d1ed25b9a745378531a3b55bb0d8197 (diff) | |
Removing spurious folder includes in coq_makefile.
Diffstat (limited to 'tools')
| -rw-r--r-- | tools/coq_makefile.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/tools/coq_makefile.ml b/tools/coq_makefile.ml index 624b9ced7..4842a8915 100644 --- a/tools/coq_makefile.ml +++ b/tools/coq_makefile.ml @@ -50,9 +50,9 @@ let section s = let lib_dirs = ["kernel"; "lib"; "library"; "parsing"; "pretyping"; "interp"; "printing"; "intf"; - "proofs"; "tactics"; "tools"; "ltacprof"; + "proofs"; "tactics"; "tools"; "vernac"; "stm"; "toplevel"; "grammar"; "config"; - "ltac"; "engine"] + "engine"] let usage () = |