From c60a65d18ef8ea715a7c5104766f1c103d2c8597 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Thu, 30 Jun 2016 22:41:29 +0200
Subject: [PATCH] Hack to avoid getting String.length instead of List.length.

In noticed in Amin's development that importing the proof mode often
turns length into String.length. The weird thing is that before importing
the proof mode, it refers to List.length, and when importing just the
proof mode, it refers to List.length too. However, in some combinations of
imports, it seems to result in it refering to String.length...
---
 theories/strings.v | 7 ++++++-
 1 file changed, 6 insertions(+), 1 deletion(-)

diff --git a/theories/strings.v b/theories/strings.v
index 31334218..6433a991 100644
--- a/theories/strings.v
+++ b/theories/strings.v
@@ -2,7 +2,12 @@
 (* This file is distributed under the terms of the BSD license. *)
 From Coq Require Import Ascii.
 From Coq Require Export String.
-From stdpp Require Export countable.
+From stdpp Require Export list.
+From stdpp Require Import countable.
+
+(* 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.
-- 
GitLab