I think I'm the one who introduced the following convention in xtla: - tla-* functions are the functions visible to the user
- tla--* functions are only for internal use. This convention is not always used as I intended initially (there are now several interactive functions named tla-- for example). Anyway, it's not easy to say wether a function or variable is internal or not (are the tla-*-cookie variables used by tla-revisions, tla-changes, tla-tree-lint, ... internal ?). So, I wonder if I shouldn't change my mind and rename all the functions as tla-*, and forget about the "double dash". What's your opinion? -- Matthieu
