diff options
| author | Matthieu Sozeau | 2016-03-17 20:23:00 +0100 |
|---|---|---|
| committer | Matthieu Sozeau | 2016-03-17 20:24:46 +0100 |
| commit | c8dcfc691a649ff6dfb3416809c6ec7b1e629b1f (patch) | |
| tree | 13c0f493133186efce01afee6715297e3479298f /dev/base_include | |
| parent | bcee0b4d6ca113d225fa7df1cbcfa33812b0bd46 (diff) | |
Fix bug #4627: records with no declared arity can be template polymorphic.
As if we were adding : Type. Consistent with inductives with no
declared arity.
Diffstat (limited to 'dev/base_include')
0 files changed, 0 insertions, 0 deletions