From 6c604e56fc179ea6155dfccf5d639f18be6599da Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Wed, 8 Apr 2020 09:50:46 +0200
Subject: [PATCH] More testing.

---
 tests/length.ref | 32 ++++++++++++++++++++++++++++++++
 tests/length.v   | 41 +++++++++++++++++++++++++++++++++++------
 2 files changed, 67 insertions(+), 6 deletions(-)

diff --git a/tests/length.ref b/tests/length.ref
index 59449dc7..170c5a2b 100644
--- a/tests/length.ref
+++ b/tests/length.ref
@@ -10,3 +10,35 @@ length
      : list ?A → nat
 where
 ?A : [ |- Type]
+length
+     : list ?A → nat
+where
+?A : [ |- Type]
+length
+     : list ?A → nat
+where
+?A : [ |- Type]
+length
+     : list ?A → nat
+where
+?A : [ |- Type]
+length
+     : list ?A → nat
+where
+?A : [ |- Type]
+length
+     : list ?A → nat
+where
+?A : [ |- Type]
+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 33612bb1..e7bebe42 100644
--- a/tests/length.v
+++ b/tests/length.v
@@ -1,7 +1,36 @@
+From stdpp Require prelude strings list.
+
 (** Check that we always get the [length] function on lists, not on strings. *)
-From stdpp Require Import prelude.
-Check length.
-From stdpp Require Import strings.
-Check length.
-From stdpp Require Import prelude.
-Check length.
\ No newline at end of file
+Module test1.
+  Import stdpp.base.
+  Check length.
+  Import stdpp.strings.
+  Check length.
+  Import stdpp.base.
+  Check length.
+End test1.
+
+Module test2.
+  Import stdpp.prelude.
+  Check length.
+  Import stdpp.strings.
+  Check length.
+  Import stdpp.prelude.
+  Check length.
+End test2.
+
+Module test3.
+  Import stdpp.strings.
+  Check length.
+  Import stdpp.prelude.
+  Check length.
+End test3.
+
+Module test4.
+  Import stdpp.list.
+  Check length.
+  Import stdpp.strings.
+  Check length.
+  Import stdpp.list.
+  Check length.
+End test4.
-- 
GitLab