From af0a1bfa3a277c15c4881bed3ceb99dda81c9362 Mon Sep 17 00:00:00 2001
From: monate
Date: Fri, 14 Mar 2003 10:24:31 +0000
Subject: notations coqide

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3768 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 ide/notations.v | 2 ++
 1 file changed, 2 insertions(+)
 create mode 100644 ide/notations.v

(limited to 'ide')

diff --git a/ide/notations.v b/ide/notations.v
new file mode 100644
index 0000000000..d0d94dc518
--- /dev/null
+++ b/ide/notations.v
@@ -0,0 +1,2 @@
+Notation "∀ x : t | P" := (x:t)P (at level 1, x,t,P at level 10).
+Notation "∃ x : t | P" := (EXT x:t|P) (at level 1, x,t,P at level 10).
-- 
cgit v1.2.3