diff options
Diffstat (limited to 'tools/coqdoc/tokens.ml')
| -rw-r--r-- | tools/coqdoc/tokens.ml | 2 |
1 files changed, 0 insertions, 2 deletions
diff --git a/tools/coqdoc/tokens.ml b/tools/coqdoc/tokens.ml index 10a105f9b..7c6c1f092 100644 --- a/tools/coqdoc/tokens.ml +++ b/tools/coqdoc/tokens.ml @@ -9,8 +9,6 @@ (* Application of printing rules based on a dictionary specific to the target language *) -open Cdglobals - (*s Dictionaries: trees annotated with string options, each node being a map from chars to dictionaries (the subtrees). A trie, in other words. |