diff options
Diffstat (limited to 'tools/coqdep_common.mli')
| -rw-r--r-- | tools/coqdep_common.mli | 5 |
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 |