From a974272fbdb5d121a4ac3e47a716d7406f8571b9 Mon Sep 17 00:00:00 2001
From: Cyril Cohen
Date: Wed, 12 Sep 2018 15:46:35 +0200
Subject: removing multiple definitions of [tT]ag*

they are already defined in ssrfun
ChangeLog updated
---
 ChangeLog | 3 +++
 1 file changed, 3 insertions(+)

(limited to 'ChangeLog')

diff --git a/ChangeLog b/ChangeLog
index a9650bc..2e8a495 100644
--- a/ChangeLog
+++ b/ChangeLog
@@ -11,6 +11,9 @@
 	  `all_iffLR` and coercion `all_iffP` (see header for doc)
 	  proved by circular implication P0 -> P1 -> ... -> Pn -> P0
 
+	* Removed duplicated definitions of `tag` `tagged` and `Tagged`
+	  from eqtype.v. They were already in ssrfun.v.
+
 24/04/2018 - compatibility with Coq 8.8 and several small fixes - version 1.7
 
 	* Added compatibility with Coq 8.8 and lost compatibility with
-- 
cgit v1.2.3