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 /tactics/tacenv.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 'tactics/tacenv.ml')
0 files changed, 0 insertions, 0 deletions