From 09f69b7c21889b288a5013df75e0d4a8e60b7df1 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Fri, 3 May 2019 23:53:27 +0200
Subject: [PATCH] Set Params and maximally implicits for `head` like other list
functions.
---
theories/list.v | 2 ++
1 file changed, 2 insertions(+)
diff --git a/theories/list.v b/theories/list.v
index ab2bb351..ab606e00 100644
--- a/theories/list.v
+++ b/theories/list.v
@@ -18,10 +18,12 @@ Notation tail := tl.
Notation take := firstn.
Notation drop := skipn.
+Arguments head {_} _ : assert.
Arguments tail {_} _ : assert.
Arguments take {_} !_ !_ / : assert.
Arguments drop {_} !_ !_ / : assert.
+Instance: Params (@head) 1 := {}.
Instance: Params (@tail) 1 := {}.
Instance: Params (@take) 1 := {}.
Instance: Params (@drop) 1 := {}.
--
GitLab