diff --git a/theories/strings.v b/theories/strings.v index 313342188ecabb096bc64da24dfbc27b74885bc7..6433a991d14a20e86f9ff7ce5ccd285adf1a9c51 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.