From 7d981af616cd0b5d779bdbcd05324417d7aba57a Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Wed, 8 Apr 2020 09:20:47 +0200
Subject: [PATCH] Fix `Export` order for `length`. Remove `length` hack in
 strings. Add a test.

---
 tests/length.ref   | 18 ++++++++++++++++++
 tests/length.v     |  7 +++++++
 theories/base.v    |  7 ++++++-
 theories/strings.v |  5 -----
 4 files changed, 31 insertions(+), 6 deletions(-)
 create mode 100644 tests/length.ref
 create mode 100644 tests/length.v

diff --git a/tests/length.ref b/tests/length.ref
new file mode 100644
index 00000000..ea57d31f
--- /dev/null
+++ b/tests/length.ref
@@ -0,0 +1,18 @@
+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
diff --git a/tests/length.v b/tests/length.v
new file mode 100644
index 00000000..e32ccb23
--- /dev/null
+++ b/tests/length.v
@@ -0,0 +1,7 @@
+(** Check that we always get the [length] function on lists, not on strings. *)
+From stdpp Require Import prelude.
+About length.
+From stdpp Require Import strings.
+About length.
+From stdpp Require Import prelude.
+About length.
\ No newline at end of file
diff --git a/theories/base.v b/theories/base.v
index b76f16a2..25c52422 100644
--- a/theories/base.v
+++ b/theories/base.v
@@ -3,7 +3,12 @@ that are used throughout the whole development. Most importantly it contains
 abstract interfaces for ordered structures, sets, and various other data
 structures. *)
 
-From Coq Require Export Morphisms RelationClasses List Bool Utf8 Setoid.
+(** The order of this [Require Export] is important: The definition of [length]
+in [List] should shadow the definition of [length] in [String]. We also need
+to export [Datatypes] because [List] contains a [parsing only] notation for
+[length], not the actual definition of [length], which is in [Datatypes]. *)
+From Coq Require Export String Datatypes List.
+From Coq Require Export Morphisms RelationClasses Bool Utf8 Setoid.
 From Coq Require Import Permutation.
 Set Default Proof Using "Type".
 Export ListNotations.
diff --git a/theories/strings.v b/theories/strings.v
index f83f075b..475603cd 100644
--- a/theories/strings.v
+++ b/theories/strings.v
@@ -1,13 +1,8 @@
 From Coq Require Import Ascii.
-From Coq Require Export String.
 From stdpp Require Export list.
 From stdpp Require Import countable.
 Set Default Proof Using "Type".
 
-(* To avoid randomly ending up with String.length because this module is
-imported hereditarily somewhere. *)
-Notation length := List.length.
-
 (** * Fix scopes *)
 Open Scope string_scope.
 (* Make sure [list_scope] has priority over [string_scope], so that
-- 
GitLab