diff options
| author | Arnaud Spiwack | 2015-01-14 12:00:24 +0100 |
|---|---|---|
| committer | Arnaud Spiwack | 2015-01-14 14:50:58 +0100 |
| commit | 1fab386bc1a96951da011de2a5490c6dbe1b7248 (patch) | |
| tree | eb92d73f0d22d7cffa1cad0a8718ba845999e3a1 /kernel/nativecode.ml | |
| parent | 61ca1ce53bf160a23fc4c8af4059d9efd742f1fb (diff) | |
Reference manual: try and improve the documentation of lazymatch.
In particular try to avoid the use of the word "backtracking" which refers to too many things.
Diffstat (limited to 'kernel/nativecode.ml')
0 files changed, 0 insertions, 0 deletions