Fix #5347: unify declaration of axioms with and without bound univs.

Note that this makes the following syntax valid:

     Axiom foo@{i} bar : Type@{i}.

(ie putting a universe declaration on the first axiom in the list, the
declaration then holds for the whole list).

1 files changed, 10 insertions, 0 deletions

diff --git a/test-suite/bugs/closed/5347.v b/test-suite/bugs/closed/5347.v
new file mode 100644
index 000000000..9267b3eb6
--- /dev/null
+++ b/test-suite/bugs/closed/5347.v
@@ -0,0 +1,10 @@
+Set Universe Polymorphism.
+
+Axiom X : Type.
+(* Used to declare [x0@{u1 u2} : X@{u1}] and [x1@{} : X@{u2}] leaving
+   the type of x1 with undeclared universes. After PR #891 this should
+   error at declaration time. *)
+Axiom x₀ x₁ : X.
+Axiom Xᵢ : X -> Type.
+
+Check Xᵢ x₁. (* conversion test raised anomaly universe undefined *)