diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2018-06-27 17:56:28 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2018-06-27 18:05:35 +0200 |
| commit | ecbd506624a1898bca658a8b1c4cfe13f1f9976c (patch) | |
| tree | 628ecd854d6a0c95250e068a182d457ef51857df /kernel | |
| parent | 51f6c9fbd1efc2af87ce9f56bc0e2056d7c9152f (diff) | |
Slightly less crazy parsing algorithm for CoqProject_file.
We use a buffer instead of O(n) appending to a string, and we also
make the parser tail-call.
Diffstat (limited to 'kernel')
0 files changed, 0 insertions, 0 deletions