From 92aceef153b80d83e9b003a76416da842a2a772c Mon Sep 17 00:00:00 2001 From: Ralf Jung <jung@mpi-sws.org> Date: Wed, 16 Sep 2020 15:30:20 +0200 Subject: [PATCH] fix base.v import order; use real import in prelude.v --- theories/base.v | 2 +- theories/prelude.v | 4 ---- 2 files changed, 1 insertion(+), 5 deletions(-) diff --git a/theories/base.v b/theories/base.v index 2c42f50f..603fe11a 100644 --- a/theories/base.v +++ b/theories/base.v @@ -10,9 +10,9 @@ we must export [Coq.Peano] later than any export of [Coq.Bool]. *) over the ones of [Coq.Peano] (see Coq PR#12950), so we import [Utf8] last. *) From Coq Require Export Morphisms RelationClasses List Bool Setoid Peano Utf8. From Coq Require Import Permutation. -From stdpp Require Import options. Export ListNotations. From Coq.Program Require Export Basics Syntax. +From stdpp Require Import options. (** This notation is necessary to prevent [length] from being printed as [strings.length] if strings.v is imported and later base.v. See diff --git a/theories/prelude.v b/theories/prelude.v index aff80807..9c18d5ee 100644 --- a/theories/prelude.v +++ b/theories/prelude.v @@ -12,8 +12,4 @@ From stdpp Require Export list list_numbers lexico. - -(* "Fake" import to whitelist this file for the check that ensures we import -this file everywhere. From stdpp Require Import options. -*) -- GitLab