From d84c26fa2eeeeb0029a56bac37bf1bae9f10882a Mon Sep 17 00:00:00 2001
From: Cyril Cohen
Date: Mon, 9 Nov 2020 13:01:18 +0100
Subject: Intro pattern extensions for dup, swap and apply

---
 CHANGELOG_UNRELEASED.md | 3 +++
 1 file changed, 3 insertions(+)

(limited to 'CHANGELOG_UNRELEASED.md')

diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md
index 46ba30d..ffc1cab 100644
--- a/CHANGELOG_UNRELEASED.md
+++ b/CHANGELOG_UNRELEASED.md
@@ -58,6 +58,9 @@ The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.0.0/).
 - Added a factory `distrLatticePOrderMixin` in order.v to build a
   `distrLatticeType` from a `porderType`.
 
+- Added intro pattern ltac views for dup, swap, apply:
+  `/[apply]`, `/[swap]` and `/[dup]`.
+
 - in `bigop.v` new lemma `sig_big_dep`, analogous to `pair_big_dep`
   but with an additional dependency in the index types `I` and `J`.
 - in `fintype.v` adds lemma `split_ordP`, a variant of `splitP` which
-- 
cgit v1.2.3