From 5f61cb231fb1b64abb26153b70fda646362cc67f 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 --- theories/base.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) 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 -- GitLab