From 66664b37be824915cc0dc6b028398e79a0aacde4 Mon Sep 17 00:00:00 2001 From: Michael Sammler <noreply@sammler.me> Date: Fri, 10 Apr 2020 09:51:10 +0200 Subject: [PATCH] another try --- theories/base.v | 14 ++++++-------- theories/strings.v | 5 +++++ 2 files changed, 11 insertions(+), 8 deletions(-) diff --git a/theories/base.v b/theories/base.v index 134a7181..9956b8bd 100644 --- a/theories/base.v +++ b/theories/base.v @@ -3,19 +3,17 @@ that are used throughout the whole development. Most importantly it contains abstract interfaces for ordered structures, sets, and various other data structures. *) -(** The order of this [Require Export] is important: The definition of [length] -in [List] should shadow the definition of [length] in [String]. We also need -to export [Datatypes] because [List] contains a [parsing only] notation for -[length], not the actual definition of [length], which is in [Datatypes]. *) -From Coq Require Export String Datatypes List. -From Coq Require Export Morphisms RelationClasses Bool Utf8 Setoid. +From Coq Require Export Morphisms RelationClasses List Bool Utf8 Setoid. From Coq Require Import Permutation. Set Default Proof Using "Type". Export ListNotations. From Coq.Program Require Export Basics Syntax. -(** TODO: This hack should be removed once we drop support for Coq 8.10. It is -needed for the transitive export/import bug that is fixed in Coq 8.11. *) +(** This notation is necessary to prevent [length] from being printed +as [strings.length] if strings.v is imported and later base.v. See +also strings.v and +https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/144 and +https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/129. *) Notation length := Datatypes.length. (** * Enable implicit generalization. *) diff --git a/theories/strings.v b/theories/strings.v index 475603cd..f83f075b 100644 --- a/theories/strings.v +++ b/theories/strings.v @@ -1,8 +1,13 @@ From Coq Require Import Ascii. +From Coq Require Export String. From stdpp Require Export list. From stdpp Require Import countable. Set Default Proof Using "Type". +(* 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. (* Make sure [list_scope] has priority over [string_scope], so that -- GitLab