Commit 26d86662 authored by Robbert Krebbers's avatar Robbert Krebbers

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...
parent 483e9a03
Pipeline #1841 passed with stage
......@@ -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.
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment