From 63c7aa195022a908e0ee43d3cfb48c836405a835 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Wed, 9 Jan 2019 13:30:04 +0100
Subject: Stop [Print] from saying [is (not) universe polymorphic].

[About] still says it.

Close #9056.
---
 test-suite/output/PatternsInBinders.out | 12 ------------
 1 file changed, 12 deletions(-)

(limited to 'test-suite/output/PatternsInBinders.out')

diff --git a/test-suite/output/PatternsInBinders.out b/test-suite/output/PatternsInBinders.out
index bdbc5a5960..8a6d94c732 100644
--- a/test-suite/output/PatternsInBinders.out
+++ b/test-suite/output/PatternsInBinders.out
@@ -1,29 +1,20 @@
 swap = fun '(x, y) => (y, x)
      : A * B -> B * A
-
-swap is not universe polymorphic
 fun '(x, y) => (y, x)
      : A * B -> B * A
 forall '(x, y), swap (x, y) = (y, x)
      : Prop
 proj_informative = fun '(exist _ x _) => x : A
      : {x : A | P x} -> A
-
-proj_informative is not universe polymorphic
 foo = fun '(Bar n b tt p) => if b then n + p else n - p
      : Foo -> nat
-
-foo is not universe polymorphic
 baz = 
 fun '(Bar n1 _ tt p1) '(Bar _ _ tt _) => n1 + p1
      : Foo -> Foo -> nat
-
-baz is not universe polymorphic
 swap = 
 fun (A B : Type) '(x, y) => (y, x)
      : forall A B : Type, A * B -> B * A
 
-swap is not universe polymorphic
 Arguments A, B are implicit and maximally inserted
 Argument scopes are [type_scope type_scope _]
 fun (A B : Type) '(x, y) => swap (x, y) = (y, x)
@@ -42,8 +33,6 @@ both_z =
 fun pat : nat * nat =>
 let '(n, p) as x := pat return (F x) in (Z n, Z p) : F (n, p)
      : forall pat : nat * nat, F pat
-
-both_z is not universe polymorphic
 fun '(x, y) '(z, t) => swap (x, y) = (z, t)
      : A * B -> B * A -> Prop
 forall '(x, y) '(z, t), swap (x, y) = (z, t)
@@ -53,7 +42,6 @@ fun (pat : nat) '(x, y) => x + y = pat
 f = fun x : nat => x + x
      : nat -> nat
 
-f is not universe polymorphic
 Argument scope is [nat_scope]
 fun x : nat => x + x
      : nat -> nat
-- 
cgit v1.2.3