diff options
Diffstat (limited to 'theories/Init/LogicSyntax.v')
| -rw-r--r-- | theories/Init/LogicSyntax.v | 20 |
1 files changed, 10 insertions, 10 deletions
diff --git a/theories/Init/LogicSyntax.v b/theories/Init/LogicSyntax.v index c652a70281..3b40228861 100644 --- a/theories/Init/LogicSyntax.v +++ b/theories/Init/LogicSyntax.v @@ -30,25 +30,25 @@ Notation "'IF' c1 'then' c2 'else' c3" := (IF c1 c2 c3) (* Order is important to give printing priority to fully typed ALL and EX *) -Notation "'ALL' x : t | p" := (all t [x:t]p) (at level 10, p at level 8) - V8only (at level 200). +Notation All := (all ?). Notation "'ALL' x | p" := (all ? [x]p) (at level 10, p at level 8) V8only (at level 200, p at level 200). -Notation All := (all ?). +Notation "'ALL' x : t | p" := (all t [x:t]p) (at level 10, p at level 8) + V8only (at level 200). -Notation "'EX' x : t | p" := (ex t [x:t]p) (at level 10, p at level 8) - V8only (at level 200, x at level 80). +Notation Ex := (ex ?). Notation "'EX' x | p" := (ex ? [x]p) (at level 10, p at level 8) V8only (at level 200, x at level 80). -Notation Ex := (ex ?). +Notation "'EX' x : t | p" := (ex t [x:t]p) (at level 10, p at level 8) + V8only (at level 200, x at level 80). -Notation "'EX' x : t | p & q" := (ex2 t [x:t]p [x:t]q) - (at level 10, p, q at level 8) - V8only "'EX2' x : t | p & q" (at level 200, x at level 80). +Notation Ex2 := (ex2 ?). Notation "'EX' x | p & q" := (ex2 ? [x]p [x]q) (at level 10, p, q at level 8) V8only "'EX2' x | p & q" (at level 200, x at level 80). -Notation Ex2 := (ex2 ?). +Notation "'EX' x : t | p & q" := (ex2 t [x:t]p [x:t]q) + (at level 10, p, q at level 8) + V8only "'EX2' x : t | p & q" (at level 200, x at level 80). (** Parsing only of things in [Logic.v] *) |