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 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

(limited to 'interp')

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
 
-- 
cgit v1.2.3