diff options
| author | Hugo Herbelin | 2017-08-14 20:53:16 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2017-09-12 20:38:44 +0200 |
| commit | 6c3fd3b8f12eb722d18b5da765bf8aec5e95ee06 (patch) | |
| tree | f10bed06914c61e6ab4d30f0f8b657291591e9c5 /kernel/nativecode.mli | |
| parent | 2e1ae2cab5a4c103ecafe7ab71b77a7ee7589760 (diff) | |
Fixing bugs of a67bd7f9 and c6d9d4fb in recognizing a 'pat binding.
Conditions for printing 'pat were incomplete.
Diffstat (limited to 'kernel/nativecode.mli')
0 files changed, 0 insertions, 0 deletions