From e1e8316aa7ea6aa0d8b21f2e4c38e5ab378f62e9 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Fri, 11 Jun 2021 13:54:12 +0200
Subject: [PATCH] Comment about `head` and `tail` notations.
---
theories/list.v | 5 +++++
1 file changed, 5 insertions(+)
diff --git a/theories/list.v b/theories/list.v
index a87d5349..ef88844b 100644
--- a/theories/list.v
+++ b/theories/list.v
@@ -15,13 +15,18 @@ Global Instance: Params (@length) 1 := {}.
Global Instance: Params (@cons) 1 := {}.
Global Instance: Params (@app) 1 := {}.
+(** [head] and [tail] are defined as [parsing only] for [hd_error] and [tl] in
+the Coq standard library. We redefine these notations to make sure they also
+pretty print properly. *)
Notation head := hd_error.
Notation tail := tl.
+
Notation take := firstn.
Notation drop := skipn.
Global Arguments head {_} _ : assert.
Global Arguments tail {_} _ : assert.
+
Global Arguments take {_} !_ !_ / : assert.
Global Arguments drop {_} !_ !_ / : assert.
--
GitLab