diff options
| author | Gaëtan Gilbert | 2018-09-14 13:35:47 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2018-09-21 13:09:21 +0200 |
| commit | 0d7643dabade293696a377dbc1f858dff2d666f4 (patch) | |
| tree | f944dffdbaacbf2f888b56e4a6068c98e7b10fb4 /test-suite | |
| parent | 138f7c628e546775b381fa1f8805acc433839684 (diff) | |
Universe binders are Id, not Name. Never print Var.
Comes with minor cleanups in exception catching and unnecessary mapi.
Diffstat (limited to 'test-suite')
| -rw-r--r-- | test-suite/output/UnivBinders.out | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/test-suite/output/UnivBinders.out b/test-suite/output/UnivBinders.out index 0f673acb79..75276c7d0e 100644 --- a/test-suite/output/UnivBinders.out +++ b/test-suite/output/UnivBinders.out @@ -86,10 +86,10 @@ Type@{M} -> Type@{N} -> Type@{E} (* E M N |= *) foo is universe polymorphic -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@{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 NonCumulative Inductive Empty@{E} : Type@{E} := |