diff options
| author | Arnaud Spiwack | 2014-09-03 16:47:54 +0200 |
|---|---|---|
| committer | Arnaud Spiwack | 2014-09-04 10:25:55 +0200 |
| commit | 06e6a7b5a0d15f493a3f94fad905af2c44be9c09 (patch) | |
| tree | e53aef545713693e2dac1710231cc9ce83caa1a9 /kernel | |
| parent | 706a4f3974c2f586ecb5d695e04e7b4f1b2e3d57 (diff) | |
Type definitions with [Variant] don't generate inductive schemes by default.
- The option [Record Elimination Schemes] is replaced by [Nonrecursive Elimination Schemes] ([Record Elimination Schemes] is kept as a deprecated option for compatibility)
- [Variant] don't generate inductive scheme unless [Nonrecursive Elimination Schemes] is turned on.
- Inductive records generate induction schemes even when [Nonrecursive Elimination Schemes] is off.
Diffstat (limited to 'kernel')
0 files changed, 0 insertions, 0 deletions