Fix bug #3825: Universe annotations on notations should pass through or be rejected.

4 files changed, 27 insertions, 3 deletions

diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index a7b1bb4128..ead68bd92f 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -767,7 +767,15 @@ let intern_qualid loc qid intern env lvar us args =
       let subst = (terms, Id.Map.empty, Id.Map.empty) in
       let infos = (Id.Map.empty, env) in
       let projapp = match c with NRef _ -> true | _ -> false in
-	subst_aconstr_in_glob_constr loc intern lvar subst infos c, projapp, args2
+      let c = subst_aconstr_in_glob_constr loc intern lvar subst infos c in
+      let c = match us, c with
+      | None, _ -> c
+      | Some _, GRef (loc, ref, None) -> GRef (loc, ref, us)
+      | Some _, _ ->
+        user_err_loc (loc, "", str "Notation " ++ pr_qualid qid ++
+          str " cannot have a universe instance")
+      in
+      c, projapp, args2
 
 (* Rule out section vars since these should have been found by intern_var *)
 let intern_non_secvar_qualid loc qid intern env lvar us args =
diff --git a/test-suite/bugs/closed/3825.v b/test-suite/bugs/closed/3825.v
new file mode 100644
index 0000000000..e594b74b62
--- /dev/null
+++ b/test-suite/bugs/closed/3825.v
@@ -0,0 +1,16 @@
+Set Universe Polymorphism.
+Set Printing Universes.
+
+Axiom foo@{i j} : Type@{i} -> Type@{j}.
+
+Notation bar := foo.
+
+Monomorphic Universes i j.
+
+Check bar@{i j}.
+Fail Check bar@{i}.
+
+Notation qux := (nat -> nat).
+
+Fail Check qux@{i}.
+
diff --git a/test-suite/bugs/closed/3922.v b/test-suite/bugs/closed/3922.v
index 5013bc6ac1..d88e8c3325 100644
--- a/test-suite/bugs/closed/3922.v
+++ b/test-suite/bugs/closed/3922.v
@@ -73,7 +73,7 @@ Definition Trunc_ind {n A}
   (P : Trunc n A -> Type) {Pt : forall aa, IsTrunc n (P aa)}
   : (forall a, P (tr a)) -> (forall aa, P aa)
 := (fun f aa => match aa with tr a => fun _ => f a end Pt).
-Definition merely (A : Type@{i}) : hProp@{i} := BuildhProp (Trunc -1 A).
+Definition merely (A : Type@{i}) : hProp := BuildhProp (Trunc -1 A).
 Definition cconst_factors_contr `{Funext}  {X Y : Type} (f : X -> Y)
            (P : Type) `{Pc : X -> Contr P}
            (g : X -> P) (h : P -> Y) (p : h o g == f)
diff --git a/test-suite/bugs/closed/4544.v b/test-suite/bugs/closed/4544.v
index d14cc86fc7..048f31ce3d 100644
--- a/test-suite/bugs/closed/4544.v
+++ b/test-suite/bugs/closed/4544.v
@@ -841,7 +841,7 @@ End Truncation_Modalities.
 
 Module Import TrM := Modalities_Theory Truncation_Modalities.
 
-Definition merely (A : Type@{i}) : hProp@{i} := BuildhProp (Trunc -1 A).
+Definition merely (A : Type@{i}) : hProp := BuildhProp (Trunc -1 A).
 
 Notation IsSurjection := (IsConnMap -1).