diff options
author | 2013-08-25 22:34:08 +0000 | |
---|---|---|
committer | 2013-08-25 22:34:08 +0000 | |
commit | f4a6a6aaa928e7a6c8d360c45268cb82c020c2dc (patch) | |
tree | 95bf369c1f34a6a4c055357b68e60de58849bd11 /parsing/lexer.ml4 | |
parent | 646c6765e5e3307f8898c4f63c405d91c2e6f47b (diff) |
Added a more efficient way to recover the domain of a map.
The extended signature is defined in CMap, and should be compatible
with the old one, except that module arguments have to be explicitely
named. The implementation itself is quite unsafe, as it relies on the
current implementation of OCaml maps, even though that should not be
a problem (it has not changed in ages).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16735 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'parsing/lexer.ml4')
-rw-r--r-- | parsing/lexer.ml4 | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/parsing/lexer.ml4 b/parsing/lexer.ml4 index 81cfd3f1d..680139b12 100644 --- a/parsing/lexer.ml4 +++ b/parsing/lexer.ml4 @@ -14,7 +14,8 @@ open Tok (* Dictionaries: trees annotated with string options, each node being a map from chars to dictionaries (the subtrees). A trie, in other words. *) -module CharMap = Map.Make (struct type t = char let compare = compare end) +module CharOrd = struct type t = char let compare : char -> char -> int = compare end +module CharMap = Map.Make (CharOrd) type ttree = { node : string option; |