diff --git a/tests/length.ref b/tests/length.ref
index ea57d31f65d6edc1ce466afdecd1ecd7127477ea..59449dc75ebc922fc894dec772af1418936b433a 100644
--- a/tests/length.ref
+++ b/tests/length.ref
@@ -1,18 +1,12 @@
-length : ∀ A : Type, list A → nat
-
-length is not universe polymorphic
-Arguments length {A}%type_scope _%list_scope
-length is transparent
-Expands to: Constant Coq.Init.Datatypes.length
-length : ∀ A : Type, list A → nat
-
-length is not universe polymorphic
-Arguments length {A}%type_scope _%list_scope
-length is transparent
-Expands to: Constant Coq.Init.Datatypes.length
-length : ∀ A : Type, list A → nat
-
-length is not universe polymorphic
-Arguments length {A}%type_scope _%list_scope
-length is transparent
-Expands to: Constant Coq.Init.Datatypes.length
+length
+     : list ?A → nat
+where
+?A : [ |- Type]
+length
+     : list ?A → nat
+where
+?A : [ |- Type]
+length
+     : list ?A → nat
+where
+?A : [ |- Type]
diff --git a/tests/length.v b/tests/length.v
index e32ccb2388504f841d3e2d9792294c357bcb0816..33612bb153156415bc79bfd90e4c821e726d0574 100644
--- a/tests/length.v
+++ b/tests/length.v
@@ -1,7 +1,7 @@
 (** Check that we always get the [length] function on lists, not on strings. *)
 From stdpp Require Import prelude.
-About length.
+Check length.
 From stdpp Require Import strings.
-About length.
+Check length.
 From stdpp Require Import prelude.
-About length.
\ No newline at end of file
+Check length.
\ No newline at end of file