diff options
| author | Pierre-Marie Pédrot | 2018-09-11 11:00:42 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2018-09-21 13:09:21 +0200 |
| commit | 51dad02266f0bea735d496839c559b472bc4553e (patch) | |
| tree | a6a18abe9b8d1ee74c848f6dcd302c08adb89da6 /test-suite | |
| parent | 4c28e0597067d81f5ee7e8b2b2e668f4d45e973f (diff) | |
Removing calls to AUContext.instance.
We simply declare the bound universes with their user-facing name in the
evarmap and call all printing functions on uninstantiated terms. We had to
tweak the universe name declaring function so that it would work properly
with bound universe variables and handle sections correctly.
This changes the output of polymorphic definitions with unnamed universe
variables. Now they are printed as Var(i) instead of the Module.n uid
that came from their absolute name.
Diffstat (limited to 'test-suite')
| -rw-r--r-- | test-suite/output/UnivBinders.out | 26 |
1 files changed, 13 insertions, 13 deletions
diff --git a/test-suite/output/UnivBinders.out b/test-suite/output/UnivBinders.out index 926114a1e1..22b998fab9 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 Top.17 v} = -Type@{Top.17} -> Type@{v} -> Type@{u} - : Type@{max(u+1,Top.17+1,v+1)} -(* u Top.17 v |= *) +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 is universe polymorphic Type@{i} -> Type@{j} @@ -86,10 +86,10 @@ Type@{M} -> Type@{N} -> Type@{E} (* E M N |= *) foo is universe polymorphic -foo@{Top.16 Top.17 Top.18} = -Type@{Top.17} -> Type@{Top.18} -> Type@{Top.16} - : Type@{max(Top.16+1,Top.17+1,Top.18+1)} -(* Top.16 Top.17 Top.18 |= *) +foo@{Var(0) Var(1) Var(2)} = +Type@{Var(1)} -> Type@{Var(2)} -> Type@{Var(0)} + : Type@{max(Var(0)+1,Var(1)+1,Var(2)+1)} +(* Var(0) Var(1) Var(2) |= *) foo is universe polymorphic NonCumulative Inductive Empty@{E} : Type@{E} := @@ -125,7 +125,7 @@ bind_univs.poly@{u} = Type@{u} bind_univs.poly is universe polymorphic insec@{v} = Type@{u} -> Type@{v} - : Type@{max(u+1,v+1)} + : Type@{max(v+1,u+1)} (* v |= *) insec is universe polymorphic @@ -155,14 +155,14 @@ inmod@{u} -> Type@{v} (* u v |= *) Applied.infunct is universe polymorphic -axfoo@{i Top.48 Top.49} : Type@{Top.48} -> Type@{i} -(* i Top.48 Top.49 |= *) +axfoo@{i Var(1) Var(2)} : Type@{Var(1)} -> Type@{i} +(* i Var(1) Var(2) |= *) axfoo is universe polymorphic Argument scope is [type_scope] Expands to: Constant Top.axfoo -axbar@{i Top.48 Top.49} : Type@{Top.49} -> Type@{i} -(* i Top.48 Top.49 |= *) +axbar@{i Var(1) Var(2)} : Type@{Var(2)} -> Type@{i} +(* i Var(1) Var(2) |= *) axbar is universe polymorphic Argument scope is [type_scope] |