From 6863389c13e85d2728c4d3c3ac40b20172e9e98b Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Mon, 9 May 2016 21:21:56 +0200
Subject: Univs: allowing notations to take univ instances

They can apply to the head reference under a notation.
---
 test-suite/bugs/closed/3825.v | 8 ++++++++
 1 file changed, 8 insertions(+)

(limited to 'test-suite')

diff --git a/test-suite/bugs/closed/3825.v b/test-suite/bugs/closed/3825.v
index e594b74b62..666c64631f 100644
--- a/test-suite/bugs/closed/3825.v
+++ b/test-suite/bugs/closed/3825.v
@@ -14,3 +14,11 @@ Notation qux := (nat -> nat).
 
 Fail Check qux@{i}.
 
+Axiom TruncType@{i} : nat -> Type@{i}.
+
+Notation "n -Type" := (TruncType n) (at level 1) : type_scope.
+Notation hProp := (0)-Type.
+
+Check hProp.
+Check hProp@{i}.
+
-- 
cgit v1.2.3