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