diff options
| author |  Enrico Tassi <Enrico.Tassi@inria.fr> | 2017-01-05 17:03:37 +0100 |
|---|---|---|
| committer | Enrico Tassi <Enrico.Tassi@inria.fr> | 2017-05-23 10:48:27 +0200 |
| commit | da5ac9169d0c65ff389104dfd983311b85e059e2 (patch) | |
| tree | 135a0285b1042779b41d3af5a7897d5ef3cfa95b /lib/coqProject_file.mli | |
| parent | 088ddea70d2d9121d76f0f3c6c0412fd2a67ff0a (diff) | |
CoqProject_file: document in API deprecated features
Diffstat (limited to 'lib/coqProject_file.mli')
| -rw-r--r-- | lib/coqProject_file.mli | 7 |
1 files changed, 5 insertions, 2 deletions
diff --git a/lib/coqProject_file.mli b/lib/coqProject_file.mli index 2bcf658fc..8c8fc068a 100644 --- a/lib/coqProject_file.mli +++ b/lib/coqProject_file.mli @@ -21,13 +21,16 @@ type project = { mllib_files : string list; mlpack_files : string list; - extra_targets : extra_target list; - subdirs : string list; ml_includes : path list; r_includes : (path * logic_path) list; q_includes : (path * logic_path) list; extra_args : string list; defs : (string * string) list; + + (* deprecated in favor of a Makefile.local using :: rules *) + extra_targets : extra_target list; + subdirs : string list; + } and extra_target = { target : string; |