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
---
 mathcomp/ssreflect/eqtype.v | 6 ------
 1 file changed, 6 deletions(-)

(limited to 'mathcomp')

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