From 3675bac6c38e0a26516e434be08bc100865b339b Mon Sep 17 00:00:00 2001
From: barras
Date: Mon, 15 Dec 2003 19:48:24 +0000
Subject: modif existentielle (exists | --> exists ,) + bug d'affichage des pt
 fixes

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5099 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 theories/Init/Datatypes.v   |  2 +-
 theories/Init/Logic.v       | 18 ++++++++---------
 theories/Init/LogicSyntax.v | 47 ---------------------------------------------
 theories/Init/Notations.v   |  2 +-
 4 files changed, 11 insertions(+), 58 deletions(-)
 delete mode 100644 theories/Init/LogicSyntax.v

(limited to 'theories/Init')

diff --git a/theories/Init/Datatypes.v b/theories/Init/Datatypes.v
index d5a1179c84..2da0d6c02a 100755
--- a/theories/Init/Datatypes.v
+++ b/theories/Init/Datatypes.v
@@ -118,4 +118,4 @@ Definition CompOpp (r:comparison) :=
   | Eq => Eq
   | Lt => Gt
   | Gt => Lt
-  end.
\ No newline at end of file
+  end.
diff --git a/theories/Init/Logic.v b/theories/Init/Logic.v
index 7cfe160a09..e225bbddbd 100755
--- a/theories/Init/Logic.v
+++ b/theories/Init/Logic.v
@@ -118,15 +118,15 @@ Definition all (A:Type) (P:A -> Prop) := forall x:A, P x.
 
 (*Rule order is important to give printing priority to fully typed ALL and EX*)
 
-Notation "'exists' x | p" := (ex (fun x => p))
-  (at level 200, x ident, p at level 99) : type_scope.
-Notation "'exists' x : t | p" := (ex (fun x:t => p))
-  (at level 200, x ident, p at level 99) : type_scope.
-
-Notation "'exists2' x | p & q" := (ex2 (fun x => p) (fun x => q))
-  (at level 200, x ident, p, q at level 99) : type_scope.
-Notation "'exists2' x : t | p & q" := (ex2 (fun x:t => p) (fun x:t => q))
-  (at level 200, x ident, t at level 200, p, q at level 99) : type_scope.
+Notation "'exists' x , p" := (ex (fun x => p))
+  (at level 200, x ident) : type_scope.
+Notation "'exists' x : t , p" := (ex (fun x:t => p))
+  (at level 200, x ident) : type_scope.
+
+Notation "'exists2' x , p & q" := (ex2 (fun x => p) (fun x => q))
+  (at level 200, x ident, p at level 200) : type_scope.
+Notation "'exists2' x : t , p & q" := (ex2 (fun x:t => p) (fun x:t => q))
+  (at level 200, x ident, t at level 200, p at level 200) : type_scope.
 
 
 (** Universal quantification *)
diff --git a/theories/Init/LogicSyntax.v b/theories/Init/LogicSyntax.v
deleted file mode 100644
index f95f56d37f..0000000000
--- a/theories/Init/LogicSyntax.v
+++ /dev/null
@@ -1,47 +0,0 @@
-(***********************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
-(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
-(*   \VV/  *************************************************************)
-(*    //   *      This file is distributed under the terms of the      *)
-(*         *       GNU Lesser General Public License Version 2.1       *)
-(***********************************************************************)
-
-(*i $Id$ i*)
-
-Require Export Notations.
-Require Export Logic.
-
-(** Symbolic notations for things in [Logic.v] *)
-
-(* Order is important to give printing priority to fully typed ALL and
-   exists *)
-
-V7only [ Notation All := (all ?). ].
-Notation "'ALL' x | p"     := (all ? [x]p)   (at level 10, p at level 8)
-  V8only "'ALL' x , p" (at level 200, p at level 200).
-Notation "'ALL' x : t | p" := (all ? [x:t]p) (at level 10, p at level 8)
-  V8only "'ALL' x : t , p" (at level 200).
-
-V7only [ Notation Ex  := (ex ?). ].
-Notation "'EX' x | p"      := (ex ? [x]p)    (at level 10, p at level 8)
-  V8only "'exists' x , p" (at level 200, x at level 99).
-Notation "'EX' x : t | p"  := (ex ? [x:t]p)  (at level 10, p at level 8)
-  V8only "'exists' x : t , p" (at level 200, x at level 99).
-
-V7only [ Notation Ex2 := (ex2 ?). ].
-Notation "'EX' x | p & q"       := (ex2 ? [x]p [x]q)
-  (at level 10, p, q at level 8)
-  V8only "'exists2' x , p & q" (at level 200, x at level 99).
-Notation "'EX' x : t | p & q"   := (ex2 ? [x:t]p [x:t]q)
-  (at level 10, p, q at level 8)
-  V8only "'exists2' x : t , p & q" (at level 200, x at level 99).
-
-V7only[
-(** Parsing only of things in [Logic.v] *)
-
-Notation "< A > 'All' ( P )" := (all A P) (A annot, at level 1, only parsing).
-Notation "< A > x = y" := (eq A x y)
-  (A annot, at level 1, x at level 0, only parsing).
-Notation "< A > x <> y" := ~(eq A x y)
-  (A annot, at level 1, x at level 0, only parsing).
-].
diff --git a/theories/Init/Notations.v b/theories/Init/Notations.v
index 05bfae722e..2a1c841656 100644
--- a/theories/Init/Notations.v
+++ b/theories/Init/Notations.v
@@ -88,4 +88,4 @@ Delimit Scope type_scope with type.
 Delimit Scope core_scope with core.
 
 Open Scope core_scope.
-Open Scope type_scope.
\ No newline at end of file
+Open Scope type_scope.
-- 
cgit v1.2.3