From e123d91faac12f9d304e7b245365ce5326e77f7a Mon Sep 17 00:00:00 2001
From: mohring
Date: Fri, 28 Mar 2003 17:25:57 +0000
Subject: notations <>, Assumption avec existentiel, replace term

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3802 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 theories/ZArith/Zsyntax.v | 3 +++
 1 file changed, 3 insertions(+)

(limited to 'theories/ZArith')

diff --git a/theories/ZArith/Zsyntax.v b/theories/ZArith/Zsyntax.v
index a0610b56d2..81c0d98170 100644
--- a/theories/ZArith/Zsyntax.v
+++ b/theories/ZArith/Zsyntax.v
@@ -260,7 +260,10 @@ Notation  "x = y = z" := x=y/\y=z
   (at level 5, y at level 4) : Z_scope
   V8only (at level 50, y at level 49).
 
+(* Now a polymorphic notation
 Notation "x <> y" := ~(eq Z x y) (at level 5, no associativity) : Z_scope.
+*)
+
 (* Notation "| x |" (Zabs x) : Z_scope.(* "|" conflicts with THENS *)*)
 
 V7only[
-- 
cgit v1.2.3