diff options
| author | Matthieu Sozeau | 2014-09-06 12:13:03 +0200 |
|---|---|---|
| committer | Matthieu Sozeau | 2014-09-06 12:13:03 +0200 |
| commit | 3ea6d6888105edd5139ae0a4d8f8ecdb586aff6c (patch) | |
| tree | c15478f2305b3055c36b4d08e1b94ba4341806a7 /plugins | |
| parent | 91274486fab8712cb6b1c338704884c102ab005a (diff) | |
Fix bug #3584, elaborating pattern-matching on primitive records to the
use of projections.
Diffstat (limited to 'plugins')
0 files changed, 0 insertions, 0 deletions