Commit c60a65d1 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 51b3e27b
......@@ -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.
......
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