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_boot.ml | |
| 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_boot.ml')
| -rw-r--r-- | tools/coqdep_boot.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/tools/coqdep_boot.ml b/tools/coqdep_boot.ml index bc3435a64..2d5fd36a6 100644 --- a/tools/coqdep_boot.ml +++ b/tools/coqdep_boot.ml @@ -25,7 +25,7 @@ let rec parse = function (* To solve conflict (e.g. same filename in kernel and checker) we allow to state an explicit order *) add_caml_dir r; - norec_dirs:=r::!norec_dirs; + norec_dirs := StrSet.add r !norec_dirs; parse ll | f :: ll -> treat_file None f; parse ll | [] -> () |