diff --git a/theories/base.v b/theories/base.v
index 25c52422cbdb63e615545170d3327375acfe7899..134a7181df3a8b7c89347543f3d15b17c4d434b9 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