From 7cfc4e5146be5666419451bdd516f1f3f264d24a Mon Sep 17 00:00:00 2001
From: Enrico Tassi <gareuselesinge@debian.org>
Date: Sun, 25 Jan 2015 14:42:51 +0100
Subject: Imported Upstream version 8.5~beta1+dfsg

---
 test-suite/output/Implicit.out | 1 +
 1 file changed, 1 insertion(+)

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

diff --git a/test-suite/output/Implicit.out b/test-suite/output/Implicit.out
index 3b65003c..0b0f501f 100644
--- a/test-suite/output/Implicit.out
+++ b/test-suite/output/Implicit.out
@@ -5,6 +5,7 @@ ex_intro (P:=fun _ : nat => True) (x:=0) I
 d2 = fun x : nat => d1 (y:=x)
      : forall x x0 : nat, x0 = x -> x0 = x
 
+d2 is not universe polymorphic
 Arguments x, x0 are implicit
 Argument scopes are [nat_scope nat_scope _]
 map id (1 :: nil)
-- 
cgit v1.2.3