diff --git a/prelude/strings.v b/prelude/strings.v index 3ace24c684a4f86e7943b26625c5d6bdb0f657f3..d935c8ed6bbdcf86c09abb2d8c8f35ab81a92ec6 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.