diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2015-07-24 18:33:11 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2015-07-24 19:34:01 +0200 |
| commit | 8a235780d9b3612e1c01323398da3e80cbbf8e9f (patch) | |
| tree | b9ae27d2d74c8a487eaa50b0e67c9fd2c8ffe8f2 /tools/coqdep_common.mli | |
| parent | d0f9a5523bf16b18bfdf8f427b0e5f005336fa39 (diff) | |
Using maps and sets instead of lists in coqdep.
The quadratic behaviour of list searching probably appears with small
enough samples. With the advent of usable libraries in Coq, and thus many
possible dependencies, better be safe than sorry.
Diffstat (limited to 'tools/coqdep_common.mli')
| -rw-r--r-- | tools/coqdep_common.mli | 6 |
1 files changed, 4 insertions, 2 deletions
diff --git a/tools/coqdep_common.mli b/tools/coqdep_common.mli index 5e5c4740c..d610a0558 100644 --- a/tools/coqdep_common.mli +++ b/tools/coqdep_common.mli @@ -6,13 +6,15 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +module StrSet : Set.S with type elt = string + val option_c : bool ref val option_noglob : bool ref val option_boot : bool ref val option_natdynlk : bool ref val option_mldep : string option ref -val norec_dirs : string list ref -val norec_dirnames : string list ref +val norec_dirs : StrSet.t ref +val norec_dirnames : StrSet.t ref val suffixe : string ref type dir = string option val ( // ) : string -> string -> string |