diff options
| author | Gaëtan Gilbert | 2018-09-14 13:38:44 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2018-09-21 13:09:21 +0200 |
| commit | 4cbbbf0842eab2a996f749957c2e5120d91d6faf (patch) | |
| tree | 15d01d2d21de2ed7a4c19d671b0be3d8d5e0fdd6 /kernel/univ.ml | |
| parent | 0d7643dabade293696a377dbc1f858dff2d666f4 (diff) | |
Add test for univ names of polymorphic inductives in sections.
This used to print Var (before #8475, even with explicit binders) but
now doesn't.
Diffstat (limited to 'kernel/univ.ml')
0 files changed, 0 insertions, 0 deletions