diff options
Diffstat (limited to 'theories/Init/Logic_TypeSyntax.v')
| -rw-r--r-- | theories/Init/Logic_TypeSyntax.v | 28 |
1 files changed, 19 insertions, 9 deletions
diff --git a/theories/Init/Logic_TypeSyntax.v b/theories/Init/Logic_TypeSyntax.v index ed915d119..08d4f47c5 100644 --- a/theories/Init/Logic_TypeSyntax.v +++ b/theories/Init/Logic_TypeSyntax.v @@ -12,29 +12,39 @@ Require Logic_Type. (** Symbolic notations for things in [Logic_type.v] *) -Notation "x == y" := (eqT ? x y) (at level 5, no associativity). -Notation "x === y" := (identityT ? x y) (at level 5, no associativity). +Notation "x == y" := (eqT ? x y) (at level 5, no associativity) + V8only (at level 50, no associativity). +Notation "x === y" := (identityT ? x y) (at level 5, no associativity) + V8only (at level 50, no associativity). (* Order is important to give printing priority to fully typed ALL and EX *) +Notation "'ALLT' x : t | p" := (allT t [x:t]p) (at level 10, p at level 8) + V8only (at level 200, x at level 80). +Notation "'ALLT' x | p" := (allT ? [x]p) (at level 10, p at level 8) + V8only (at level 200, x at level 80). Notation AllT := (allT ?). -Notation "'ALLT' x : t | p" := (allT t [x:t]p) (at level 10, p at level 8). -Notation "'ALLT' x | p" := (allT ? [x]p) (at level 10, p at level 8). +Notation "'EXT' x : t | p" := (exT t [x:t]p) (at level 10, p at level 8) + V8only (at level 200, x at level 80). +Notation "'EXT' x | p" := (exT ? [x]p) (at level 10, p at level 8) + V8only (at level 200, x at level 80). Notation ExT := (exT ?). -Notation "'EXT' x : t | p" := (exT t [x:t]p) (at level 10, p at level 8). -Notation "'EXT' x | p" := (exT ? [x]p) (at level 10, p at level 8). -Notation ExT2 := (exT2 ?). Notation "'EXT' x : t | p & q" := (exT2 t [x:t]p [x:t]q) - (at level 10, p, q at level 8). + (at level 10, p, q at level 8) + V8only "'EXT2' x : t | p & q" (at level 200, x at level 80). Notation "'EXT' x | p & q" := (exT2 ? [x]p [x]q) - (at level 10, p, q at level 8). + (at level 10, p, q at level 8) + V8only "'EXT2' x | p & q" (at level 200, x at level 80). +Notation ExT2 := (exT2 ?). (** Parsing only of things in [Logic_type.v] *) +V7only[ Notation "< A > x == y" := (eqT A x y) (A annot, at level 1, x at level 0, only parsing). Notation "< A > x === y" := (identityT A x y) (A annot, at level 1, x at level 0, only parsing). +]. |