diff options
| author | Hugo Herbelin | 2020-10-03 16:40:57 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2020-11-21 16:45:21 +0100 |
| commit | a20d7312897cc9b4f580b68d1d6cefdfd0c5ead3 (patch) | |
| tree | 9711167af3807c4fd3152cd35020bb44b524fa1d /pretyping/reductionops.ml | |
| parent | 35ff578d093b3616af1280dd768e2afc96a8e09e (diff) | |
Unification: documenting eta for pi-types and record types.
We also align their type on (more) standard invariants.
Diffstat (limited to 'pretyping/reductionops.ml')
0 files changed, 0 insertions, 0 deletions