From f3842eb3504a6b808bf2e9006bb973321efd9045 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Wed, 8 Apr 2020 09:34:29 +0200
Subject: [PATCH] Use `Check` instead of `About` to hopefully have stable test
 output among Coq versions.

---
 tests/length.ref | 30 ++++++++++++------------------
 tests/length.v   |  6 +++---
 2 files changed, 15 insertions(+), 21 deletions(-)

diff --git a/tests/length.ref b/tests/length.ref
index ea57d31f..59449dc7 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 e32ccb23..33612bb1 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
-- 
GitLab