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 | |
parent | 088ddea70d2d9121d76f0f3c6c0412fd2a67ff0a (diff) |
CoqProject_file: document in API deprecated features
Diffstat (limited to 'lib')
-rw-r--r-- | lib/coqProject_file.ml4 | 5 | ||||
-rw-r--r-- | lib/coqProject_file.mli | 7 |
2 files changed, 8 insertions, 4 deletions
diff --git a/lib/coqProject_file.ml4 b/lib/coqProject_file.ml4 index 9327f173e..64076d604 100644 --- a/lib/coqProject_file.ml4 +++ b/lib/coqProject_file.ml4 @@ -19,13 +19,14 @@ 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; + + extra_targets : extra_target list; + subdirs : string list; } and extra_target = { target : string; 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; |