diff options
| author | Jan-Oliver Kaiser | 2020-05-15 11:44:29 +0200 |
|---|---|---|
| committer | Pierre Roux | 2021-04-22 09:16:22 +0200 |
| commit | 9b35db9c7eb0cbc8e27c67f2ba2783fdd28ba247 (patch) | |
| tree | 0082a2c5155f71fbbfa6c5ab6cde822865cbf476 /kernel/inductive.ml | |
| parent | 2cbc36c6ae4ca22e000dbb045c865f54a454aca3 (diff) | |
Extend Canonical Structure documentation.
This commit adds a more detailed explanation of what kinds of terms are
allowed in fields of a canonical instance, how the fields are used as
keys for canonical extension, what terms are considered overlapping, and
how Coq reacts to overlapping fields.
Diffstat (limited to 'kernel/inductive.ml')
0 files changed, 0 insertions, 0 deletions