From 26d866621c148851c156efc741b6b6ad86b15192 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...
---
 prelude/strings.v | 7 ++++++-
 1 file changed, 6 insertions(+), 1 deletion(-)

diff --git a/prelude/strings.v b/prelude/strings.v
index 3ace24c68..d935c8ed6 100644
--- a/prelude/strings.v
+++ b/prelude/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 iris.prelude Require Export countable.
+From iris.prelude Require Export list.
+From iris.prelude 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