From 360a8819a08c4cf005d96f0ac6bff65903dccfd4 Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Mon, 3 Sep 2018 15:02:21 +0200
Subject: [warnings] -w "+compatibility-notation" clean

---
 mathcomp/ssreflect/eqtype.v | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

(limited to 'mathcomp/ssreflect/eqtype.v')

diff --git a/mathcomp/ssreflect/eqtype.v b/mathcomp/ssreflect/eqtype.v
index 01ce7a9..7721f0e 100644
--- a/mathcomp/ssreflect/eqtype.v
+++ b/mathcomp/ssreflect/eqtype.v
@@ -784,9 +784,9 @@ Canonical option_eqType := Eval hnf in EqType (option T) option_eqMixin.
 
 End OptionEqType.
 
-Definition tag := projS1.
-Definition tagged I T_ :  forall u, T_(tag u) := @projS2 I [eta T_].
-Definition Tagged I i T_ x := @existS I [eta T_] i x.
+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.
 
-- 
cgit v1.2.3