Use `Check` instead of `About` to hopefully have stable test output among Coq versions.

tests/length.ref

-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]

tests/length.v

 (** 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.
+Check length.
\ No newline at end of file