From 7e05d4eacd3d9435f930f6e97e0260e0194e328a Mon Sep 17 00:00:00 2001
From: msozeau
Date: Mon, 10 Apr 2006 16:33:52 +0000
Subject: Fixes for new unification, not used in default version as it really
 changes unification.

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

(limited to 'contrib/subtac/FixSub.v')

diff --git a/contrib/subtac/FixSub.v b/contrib/subtac/FixSub.v
index a9a22ca76e..bbf722dbb2 100644
--- a/contrib/subtac/FixSub.v
+++ b/contrib/subtac/FixSub.v
@@ -20,11 +20,3 @@ Definition Fix_sub (x : A) := Fix_F_sub x (Rwf x).
 End FixPoint.
 
 End Well_founded.
-
-Notation "'forall' { x : A | P } , Q" :=
-  (forall x:{x:A|P}, Q)
-  (at level 200, x ident, right associativity).
-
-Notation "'fun' { x : A | P } => Q" :=
-  (fun x:{x:A|P} => Q)
-  (at level 200, x ident, right associativity).
-- 
cgit v1.2.3