diff options
Diffstat (limited to 'theories/Init')
| -rwxr-xr-x | theories/Init/Datatypes.v | 2 | ||||
| -rwxr-xr-x | theories/Init/Logic.v | 18 | ||||
| -rw-r--r-- | theories/Init/LogicSyntax.v | 47 | ||||
| -rw-r--r-- | theories/Init/Notations.v | 2 |
4 files changed, 11 insertions, 58 deletions
diff --git a/theories/Init/Datatypes.v b/theories/Init/Datatypes.v index d5a1179c8..2da0d6c02 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 7cfe160a0..e225bbddb 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 f95f56d37..000000000 --- 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 05bfae722..2a1c84165 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. |