From 0d7643dabade293696a377dbc1f858dff2d666f4 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Fri, 14 Sep 2018 13:35:47 +0200
Subject: Universe binders are Id, not Name. Never print Var.

Comes with minor cleanups in exception catching and unnecessary mapi.
---
 test-suite/output/UnivBinders.out | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

(limited to 'test-suite')

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} :=  
-- 
cgit v1.2.3