diff options
| author | barras | 2003-10-16 20:35:47 +0000 |
|---|---|---|
| committer | barras | 2003-10-16 20:35:47 +0000 |
| commit | b6b9cf860878bd39dafd1f1edb2d212eb67ba7a1 (patch) | |
| tree | b5d214119636ecfcfbace4b1da56dd2c07ac480e /theories/Init | |
| parent | b0a0a13254dcb742b8f1f519b1445c73040f5996 (diff) | |
nouvelle syntaxe de ltac
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4661 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/Init')
| -rw-r--r-- | theories/Init/Notations.v | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/theories/Init/Notations.v b/theories/Init/Notations.v index 0b7b630e47..8a107f5c08 100644 --- a/theories/Init/Notations.v +++ b/theories/Init/Notations.v @@ -85,7 +85,7 @@ Uninterpreted Notation "B + { x : A & P & Q }" (* At level 1 to factor with {x:A|P} etc *) Uninterpreted Notation "{ A } + { B }" (at level 1) - V8only (at level 10, A at level 80). + V8only (at level 0, A at level 80). Uninterpreted Notation "A + { B }" (at level 4, left associativity) V8only (at level 40, B at level 80, left associativity). @@ -93,13 +93,13 @@ Uninterpreted Notation "A + { B }" (at level 4, left associativity) (** Notations for sigma-types or subsets *) Uninterpreted Notation "{ x : A | P }" (at level 1) - V8only (at level 10, x at level 80). + V8only (at level 0, x at level 80). Uninterpreted Notation "{ x : A | P & Q }" (at level 1) - V8only (at level 10, x at level 80). + V8only (at level 0, x at level 80). Uninterpreted Notation "{ x : A & P }" (at level 1) - V8only (at level 10, x at level 80). + V8only (at level 0, x at level 80). Uninterpreted Notation "{ x : A & P & Q }" (at level 1) - V8only (at level 10, x at level 80). + V8only (at level 0, x at level 80). Delimits Scope type_scope with T. |