diff options
| author | Arnaud Spiwack | 2015-01-14 12:10:01 +0100 |
|---|---|---|
| committer | Arnaud Spiwack | 2015-01-14 14:50:58 +0100 |
| commit | b63549edce71492617db99a75410256f1b0239b0 (patch) | |
| tree | 019137edfd4641b2aafc0be23d86ebb6456295b5 /kernel/nativecode.ml | |
| parent | 1fab386bc1a96951da011de2a5490c6dbe1b7248 (diff) | |
Reference manual: try and improve documentation for Ltac's match.
In particular document the "once" behaviour.
Diffstat (limited to 'kernel/nativecode.ml')
0 files changed, 0 insertions, 0 deletions