diff options
| author | Pierre-Marie Pédrot | 2016-12-04 21:48:06 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2017-05-19 15:17:31 +0200 |
| commit | 07ad1ca45473ba02db9b687bb7e89d440ba79b20 (patch) | |
| tree | 010c25d3f0c4c3d105d15eea15682977ac9b79c3 /Control.v | |
| parent | 2dc3175916f3968d4cdba9af140fbc2667ff70a5 (diff) | |
Proper handling of record types.
We add the standard ML facilities for records, that is, projections,
mutable fields and primitive to set them.
Diffstat (limited to 'Control.v')
0 files changed, 0 insertions, 0 deletions