aboutsummaryrefslogtreecommitdiffhomepage
path: root/tools/coqdep_common.mli
diff options
context:
space:
mode:
authorGravatar Maxime Dénès <mail@maximedenes.fr>2016-07-05 18:22:53 +0200
committerGravatar Maxime Dénès <mail@maximedenes.fr>2016-07-05 18:29:00 +0200
commitb2dd4dd979577e4f384750872f7f0e7f9bd8df94 (patch)
tree613c86859810558ec7127a47fc6469ec207b7ca5 /tools/coqdep_common.mli
parent82ed3089485ebe0b722d8505ddbd89d73570b8f9 (diff)
Revert "Merge remote-tracking branch 'github/pr/229' into trunk"
This reverts commit b2f8f9edd5c1bb0a9c8c4f4b049381b979d3e385, reversing changes made to da99355b4d6de31aec5a660f7afe100190a8e683. Hugo asked for more discussion on this topic, and it was not in the roadmap. I merged it prematurely because I thought there was a consensus. Also, I missed that it was changing coq_makefile. Sorry about that.
Diffstat (limited to 'tools/coqdep_common.mli')
-rw-r--r--tools/coqdep_common.mli5
1 files changed, 1 insertions, 4 deletions
diff --git a/tools/coqdep_common.mli b/tools/coqdep_common.mli
index 205e99176..633c474ad 100644
--- a/tools/coqdep_common.mli
+++ b/tools/coqdep_common.mli
@@ -19,10 +19,7 @@ val find_dir_logpath: string -> string list
val option_c : bool ref
val option_noglob : bool ref
val option_boot : bool ref
-
-type dynlink = Opt | Byte | Both | No | Variable
-
-val option_dynlink : dynlink ref
+val option_natdynlk : bool ref
val option_mldep : string option ref
val norec_dirs : StrSet.t ref
val suffixe : string ref