From 26a79004e47bbdc97df61015ce7e944eef14ac71 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Mon, 8 Sep 2014 10:23:12 +0200
Subject: Parsing of Type@{max(i,j)}.

---
 test-suite/success/namedunivs.v | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

(limited to 'test-suite')

diff --git a/test-suite/success/namedunivs.v b/test-suite/success/namedunivs.v
index 5c0a3c7f23..059462fac3 100644
--- a/test-suite/success/namedunivs.v
+++ b/test-suite/success/namedunivs.v
@@ -30,6 +30,9 @@ Definition foo' {A : Type@{i}} (o : option@{i} A) : option@{i} A :=
 Definition foo'' {A : Type@{i}} (o : option@{j} A) : option@{k} A :=
   o.
 
+
+Definition testm (A : Type@{i}) : Type@{max(i,j)} := A.
+
 (* Inductive prod (A : Type@{i}) (B : Type@{j}) := *)
 (*   | pair : A -> B -> prod A B. *)
 
@@ -43,7 +46,6 @@ Definition foo'' {A : Type@{i}} (o : option@{j} A) : option@{k} A :=
 (*     | pair _ _ a b => b *)
 (*   end. *)
 
-
 (* Inductive paths {A : Type} : A -> A -> Type := *)
 (* | idpath (a : A) : paths a a. *)
 
-- 
cgit v1.2.3