diff options
| author | Hugo Herbelin | 2017-05-20 18:08:24 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2017-05-31 00:44:26 +0200 |
| commit | 99fe89385f6590aac5bc2dadf246c3d021986f7c (patch) | |
| tree | 6c122c59d5a1637c03dbb5d6dd975af3b41702ba /dev | |
| parent | bcc9165aec1a80d563d7060ef127ad022e9ed008 (diff) | |
Using EConstr and more invariants in record.ml.
Diffstat (limited to 'dev')
0 files changed, 0 insertions, 0 deletions