diff --git a/theories/list.v b/theories/list.v
index 85164d2f360bbe69fd8aa82f822af83cfb4a94e2..f6ab979bbfae860177c5161404846e01ffdcf477 100644
--- a/theories/list.v
+++ b/theories/list.v
@@ -15,6 +15,7 @@ Global Instance: Params (@length) 1 := {}.
 Global Instance: Params (@cons) 1 := {}.
 Global Instance: Params (@app) 1 := {}.
 
+Notation head := hd_error.
 Notation tail := tl.
 Notation take := firstn.
 Notation drop := skipn.