From 22a614b0f2723cdff1223d989099f3f20bed2ff9 Mon Sep 17 00:00:00 2001
From: msozeau
Date: Sun, 11 Mar 2007 09:53:04 +0000
Subject: Remove bugguy notations

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9695 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 contrib/subtac/Utils.v | 4 ----
 1 file changed, 4 deletions(-)

diff --git a/contrib/subtac/Utils.v b/contrib/subtac/Utils.v
index 0a28ac45ba..6250794526 100644
--- a/contrib/subtac/Utils.v
+++ b/contrib/subtac/Utils.v
@@ -66,7 +66,3 @@ Extract Inductive sigT => "pair" [ "" ].
 Require Export ProofIrrelevance.
 
 Delimit Scope program_scope with program.
-
-Require Import Specif.
-Notation "'left'" := (left _ _) : program_scope.
-Notation "'right'" := (right _ _) : program_scope.
-- 
cgit v1.2.3