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 +++
 mathcomp/ssreflect/eqtype.v | 6 ------
 2 files changed, 3 insertions(+), 6 deletions(-)

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
diff --git a/mathcomp/ssreflect/eqtype.v b/mathcomp/ssreflect/eqtype.v
index 7721f0e..7c2a48e 100644
--- a/mathcomp/ssreflect/eqtype.v
+++ b/mathcomp/ssreflect/eqtype.v
@@ -784,12 +784,6 @@ Canonical option_eqType := Eval hnf in EqType (option T) option_eqMixin.
 
 End OptionEqType.
 
-Definition tag := projT1.
-Definition tagged I T_ :  forall u, T_(tag u) := @projT2 I [eta T_].
-Definition Tagged I i T_ x := @existT I [eta T_] i x.
-Arguments Tagged [I i].
-Prenex Implicits tag tagged Tagged.
-
 Section TaggedAs.
 
 Variables (I : eqType) (T_ : I -> Type).
-- 
cgit v1.2.3