From 8a235780d9b3612e1c01323398da3e80cbbf8e9f Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Fri, 24 Jul 2015 18:33:11 +0200 Subject: 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. --- tools/coqdep_common.mli | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) (limited to 'tools/coqdep_common.mli') 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 -- cgit v1.2.3