diff options
| author | Pierre-Marie Pédrot | 2018-09-13 15:14:01 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2018-09-21 13:09:21 +0200 |
| commit | 138f7c628e546775b381fa1f8805acc433839684 (patch) | |
| tree | 7c3812765e5d28a4574ad220c3cc87824546e7c5 /test-suite | |
| parent | aaee23f06e4ac345238cb84edc1c16fafe6b6b3d (diff) | |
Best-effort hack to provide a meaningful name for anonymous bound universes.
This restores the old behaviour that was printing qualified global names as
a representation of anonymous bound universes, at the cost of a ugly hack.
Ideally this should be handled by the callers, but for the time being the
trade-off is probably OK.
Diffstat (limited to 'test-suite')
| -rw-r--r-- | test-suite/output/UnivBinders.out | 16 |
1 files changed, 8 insertions, 8 deletions
diff --git a/test-suite/output/UnivBinders.out b/test-suite/output/UnivBinders.out index 22b998fab9..0f673acb79 100644 --- a/test-suite/output/UnivBinders.out +++ b/test-suite/output/UnivBinders.out @@ -42,10 +42,10 @@ bar@{u} = nat *) bar is universe polymorphic -foo@{u Var(1) v} = -Type@{Var(1)} -> Type@{v} -> Type@{u} - : Type@{max(u+1,Var(1)+1,v+1)} -(* u Var(1) v |= *) +foo@{u Top.17 v} = +Type@{Top.17} -> Type@{v} -> Type@{u} + : Type@{max(u+1,Top.17+1,v+1)} +(* u Top.17 v |= *) foo is universe polymorphic Type@{i} -> Type@{j} @@ -155,14 +155,14 @@ inmod@{u} -> Type@{v} (* u v |= *) Applied.infunct is universe polymorphic -axfoo@{i Var(1) Var(2)} : Type@{Var(1)} -> Type@{i} -(* i Var(1) Var(2) |= *) +axfoo@{i Top.48 Top.49} : Type@{Top.48} -> Type@{i} +(* i Top.48 Top.49 |= *) axfoo is universe polymorphic Argument scope is [type_scope] Expands to: Constant Top.axfoo -axbar@{i Var(1) Var(2)} : Type@{Var(2)} -> Type@{i} -(* i Var(1) Var(2) |= *) +axbar@{i Top.48 Top.49} : Type@{Top.49} -> Type@{i} +(* i Top.48 Top.49 |= *) axbar is universe polymorphic Argument scope is [type_scope] |