From 0aa2544d04dbd4b6ee665b551ed165e4fb02d2fa Mon Sep 17 00:00:00 2001
From: Enrico Tassi <gareuselesinge@debian.org>
Date: Wed, 15 Jul 2015 10:36:12 +0200
Subject: Imported Upstream version 8.5~beta2+dfsg

---
 test-suite/output/inference.out | 2 --
 1 file changed, 2 deletions(-)

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

diff --git a/test-suite/output/inference.out b/test-suite/output/inference.out
index d69baaec..b1952aec 100644
--- a/test-suite/output/inference.out
+++ b/test-suite/output/inference.out
@@ -4,8 +4,6 @@ fun e : option L => match e with
                     | None => None
                     end
      : option L -> option L
-
-P is not universe polymorphic
 fun (m n p : nat) (H : S m <= S n + p) => le_S_n m (n + p) H
      : forall m n p : nat, S m <= S n + p -> m <= n + p
 fun n : nat => let x := A n in ?y ?y0:T n
-- 
cgit v1.2.3