5 files changed, 46 insertions, 7 deletions

diff --git a/interp/constrexpr_ops.ml b/interp/constrexpr_ops.ml
index d4369e9bd1..d6097304ec 100644
--- a/interp/constrexpr_ops.ml
+++ b/interp/constrexpr_ops.ml
@@ -121,9 +121,10 @@ let rec constr_expr_eq e1 e2 =
       constr_expr_eq a1 a2 &&
       Option.equal constr_expr_eq t1 t2 &&
       constr_expr_eq b1 b2
-    | CAppExpl((proj1,r1,_),al1), CAppExpl((proj2,r2,_),al2) ->
+    | CAppExpl((proj1,r1,u1),al1), CAppExpl((proj2,r2,u2),al2) ->
       Option.equal Int.equal proj1 proj2 &&
       qualid_eq r1 r2 &&
+      eq_universes u1 u2 &&
       List.equal constr_expr_eq al1 al2
     | CApp((proj1,e1),al1), CApp((proj2,e2),al2) ->
       Option.equal Int.equal proj1 proj2 &&
@@ -158,8 +159,8 @@ let rec constr_expr_eq e1 e2 =
       Id.equal id1 id2 && List.equal instance_eq c1 c2
     | CSort s1, CSort s2 ->
       Glob_ops.glob_sort_eq s1 s2
-  | CCast(t1,c1), CCast(t2,c2) ->
-    constr_expr_eq t1 t2 && cast_expr_eq c1 c2
+    | CCast(t1,c1), CCast(t2,c2) ->
+      constr_expr_eq t1 t2 && cast_expr_eq c1 c2
     | CNotation(inscope1, n1, s1), CNotation(inscope2, n2, s2) ->
       Option.equal notation_with_optional_scope_eq inscope1 inscope2 &&
       notation_eq n1 n2 &&
diff --git a/pretyping/glob_ops.ml b/pretyping/glob_ops.ml
index a006c82993..cb868e0480 100644
--- a/pretyping/glob_ops.ml
+++ b/pretyping/glob_ops.ml
@@ -60,12 +60,20 @@ let glob_sort_family = let open Sorts in function
   | UNamed [GSet,0] -> InSet
   | _ -> raise ComplexSort
 
-let glob_sort_eq u1 u2 = match u1, u2 with
+let glob_sort_expr_eq f u1 u2 =
+ match u1, u2 with
   | UAnonymous {rigid=r1}, UAnonymous {rigid=r2} -> r1 = r2
-  | UNamed l1, UNamed l2 ->
-    List.equal (fun (x,m) (y,n) -> glob_sort_name_eq x y && Int.equal m n) l1 l2
+  | UNamed l1, UNamed l2 -> f l1 l2
   | (UNamed _ | UAnonymous _), _ -> false
 
+let glob_sort_eq u1 u2 =
+  glob_sort_expr_eq
+    (List.equal (fun (x,m) (y,n) -> glob_sort_name_eq x y && Int.equal m n))
+    u1 u2
+
+let glob_level_eq u1 u2 =
+  glob_sort_expr_eq glob_sort_name_eq u1 u2
+
 let binding_kind_eq bk1 bk2 = match bk1, bk2 with
   | Explicit, Explicit -> true
   | NonMaxImplicit, NonMaxImplicit -> true
@@ -123,7 +131,9 @@ let instance_eq f (x1,c1) (x2,c2) =
   Id.equal x1 x2 && f c1 c2
 
 let mk_glob_constr_eq f c1 c2 = match DAst.get c1, DAst.get c2 with
-  | GRef (gr1, _), GRef (gr2, _) -> GlobRef.equal gr1 gr2
+  | GRef (gr1, u1), GRef (gr2, u2) ->
+    GlobRef.equal gr1 gr2 &&
+    Option.equal (List.equal glob_level_eq) u1 u2
   | GVar id1, GVar id2 -> Id.equal id1 id2
   | GEvar (id1, arg1), GEvar (id2, arg2) ->
     Id.equal id1 id2 && List.equal (instance_eq f) arg1 arg2
diff --git a/pretyping/glob_ops.mli b/pretyping/glob_ops.mli
index 14bf2f6764..6da8173dce 100644
--- a/pretyping/glob_ops.mli
+++ b/pretyping/glob_ops.mli
@@ -15,6 +15,8 @@ open Glob_term
 
 val glob_sort_eq : Glob_term.glob_sort -> Glob_term.glob_sort -> bool
 
+val glob_level_eq : Glob_term.glob_level -> Glob_term.glob_level -> bool
+
 val cases_pattern_eq : 'a cases_pattern_g -> 'a cases_pattern_g -> bool
 
 (** Expect a Prop/SProp/Set/Type universe; raise [ComplexSort] if
diff --git a/test-suite/output/bug_11934.out b/test-suite/output/bug_11934.out
new file mode 100644
index 0000000000..072136c82e
--- /dev/null
+++ b/test-suite/output/bug_11934.out
@@ -0,0 +1,13 @@
+thing = forall x y : foo, bla x y
+     : Prop
+thing = 
+forall (x : foo@{thing.u0}) (y : foo@{thing.u1}), bla x y
+     : Prop
+(* {thing.u1 thing.u0} |= bla.u0 = thing.u0
+                          bla.u1 = thing.u1 *)
+thing = 
+forall (x : @foo@{thing.u0} True) (y : @foo@{thing.u1} True),
+@bla True True x y
+     : Prop
+(* {thing.u1 thing.u0} |= bla.u0 = thing.u0
+                          bla.u1 = thing.u1 *)
diff --git a/test-suite/output/bug_11934.v b/test-suite/output/bug_11934.v
new file mode 100644
index 0000000000..fe9772dc62
--- /dev/null
+++ b/test-suite/output/bug_11934.v
@@ -0,0 +1,13 @@
+Polymorphic Axiom foo@{u} : Prop -> Prop.
+Arguments foo {_}.
+
+Axiom bla : forall {A B}, @foo A -> @foo B -> Prop.
+Definition thing := forall (x:@foo@{Type} True) (y:@foo@{Type} True), bla x y.
+
+Print thing. (* forall x y : foo, bla x y *)
+
+Set Printing Universes.
+Print thing. (* forall (x : foo@{thing.u0}) (y : foo@{thing.u1}), bla x y *)
+
+Set Printing Implicit.
+Print thing. (* BAD: forall x y : @foo@{thing.u0} True, @bla True True x y *)