From dc849367323895264ae3b337e60ffa6f029b1c9b Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Wed, 8 Apr 2020 09:49:50 +0200
Subject: [PATCH] =?UTF-8?q?`length`=20notation=20in=20`base`=20to=20also?=
=?UTF-8?q?=20fix=20`length`=20in=20Coq=20=E2=89=A4=208.10.?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit
---
theories/base.v | 4 ++++
1 file changed, 4 insertions(+)
diff --git a/theories/base.v b/theories/base.v
index 25c52422..134a7181 100644
--- a/theories/base.v
+++ b/theories/base.v
@@ -14,6 +14,10 @@ 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. *)
+Notation length := Datatypes.length.
+
(** * Enable implicit generalization. *)
(** This option enables implicit generalization in arguments of the form
`{...} (i.e., anonymous arguments). Unfortunately, it also enables
--
GitLab