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.
---
 interp/constrintern.ml        | 5 ++++-
 test-suite/bugs/closed/3825.v | 8 ++++++++
 2 files changed, 12 insertions(+), 1 deletion(-)

diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index b6fce61781..f30d3cefad 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -777,9 +777,12 @@ let intern_qualid loc qid intern env lvar us args =
       let c = match us, c with
       | None, _ -> c
       | Some _, GRef (loc, ref, None) -> GRef (loc, ref, us)
+      | Some _, GApp (loc, GRef (loc', ref, None), arg) ->
+         GApp (loc, GRef (loc', ref, us), arg)
       | Some _, _ ->
         user_err_loc (loc, "", str "Notation " ++ pr_qualid qid ++
-          str " cannot have a universe instance")
+          str " cannot have a universe instance, its expanded head
+               does not start with a reference")
       in
       c, projapp, args2
 
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