From f3c4eb0ab319e1dd95bdc49ae3e472f5cdb6967f Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Fri, 11 Jun 2021 12:02:31 +0200
Subject: [PATCH] Define `head` as notation that also prints (Coq defines it as
`parsing only`).
---
theories/list.v | 1 +
1 file changed, 1 insertion(+)
diff --git a/theories/list.v b/theories/list.v
index 85164d2f..f6ab979b 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.
--
GitLab