diff options
| author | Arnaud Spiwack | 2015-01-14 12:00:24 +0100 |
|---|---|---|
| committer | Arnaud Spiwack | 2015-01-14 15:00:03 +0100 |
| commit | 9d5e80b3478964e0e40c139a75b8ef4013efabcf (patch) | |
| tree | 6d22ea827a33935b6e54dd11388bd25ead678795 /kernel/nativecode.ml | |
| parent | 9b6b7b3608ba15df55f8073e182c36cdb94f55b7 (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