From cae7897048108d9c219f736b5ba0829e8321e258 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Fri, 11 Jun 2021 00:14:02 +0200
Subject: [PATCH] Make sure `tail` is not `simpl`ed too much.

---
 theories/list.v | 1 +
 1 file changed, 1 insertion(+)

diff --git a/theories/list.v b/theories/list.v
index 63a3ce6a..a9781689 100644
--- a/theories/list.v
+++ b/theories/list.v
@@ -168,6 +168,7 @@ if the list [l] is empty. *)
 Fixpoint last {A} (l : list A) : option A :=
   match l with [] => None | [x] => Some x | _ :: l => last l end.
 Global Instance: Params (@last) 1 := {}.
+Global Arguments last : simpl nomatch.
 
 (** The function [resize n y l] takes the first [n] elements of [l] in case
 [length l ≤ n], and otherwise appends elements with value [x] to [l] to obtain
-- 
GitLab