diff options
| author | Pierre-Marie Pédrot | 2014-07-03 10:34:29 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2014-07-03 16:07:59 +0200 |
| commit | b17fb013f1810106b8cd88a12a2df3f26dc7c289 (patch) | |
| tree | 60ee5af1548858855b00a15c92acec384b03303f /kernel/nativecode.mli | |
| parent | f222f46e7d231c5afe72e146de92dc8dcadbdcb6 (diff) | |
More efficient implementation of Ltac match, by inlining a stream map.
Diffstat (limited to 'kernel/nativecode.mli')
0 files changed, 0 insertions, 0 deletions