From f5bdbc026f6aa9456aa3850451942f72f9c9190e Mon Sep 17 00:00:00 2001
From: herbelin
Date: Mon, 31 Mar 2003 12:41:40 +0000
Subject: Notation eqT superflue

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3816 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 theories/Init/Logic_TypeSyntax.v | 2 --
 1 file changed, 2 deletions(-)

diff --git a/theories/Init/Logic_TypeSyntax.v b/theories/Init/Logic_TypeSyntax.v
index 9cebfb7df9..fa5ab26f8a 100644
--- a/theories/Init/Logic_TypeSyntax.v
+++ b/theories/Init/Logic_TypeSyntax.v
@@ -15,8 +15,6 @@ Require Logic_Type.
 Notation "x == y"  := (eq ? x y) (at level 5, no associativity, only parsing).
 Notation "x === y" := (identityT ? x y) (at level 5, no associativity).
 
-Notation "'eqT'" := eq (at level 0).
-
 (* Order is important to give printing priority to fully typed ALL and EX *)
 
 Notation AllT := (all ?).
-- 
cgit v1.2.3