diff options
| author | herbelin | 2002-12-15 12:32:15 +0000 |
|---|---|---|
| committer | herbelin | 2002-12-15 12:32:15 +0000 |
| commit | 356c712e811c23e496ace3684b3345972b5d8f71 (patch) | |
| tree | be914a487220e9083f5d9f7cd901146f54dfbcb7 | |
| parent | 1487dfbba585133f8776f02c14d49634d802919f (diff) | |
Ajout syntaxe '>'
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3444 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | theories/Init/PeanoSyntax.v | 15 |
1 files changed, 8 insertions, 7 deletions
diff --git a/theories/Init/PeanoSyntax.v b/theories/Init/PeanoSyntax.v index adb917b765..de3bac0d8e 100644 --- a/theories/Init/PeanoSyntax.v +++ b/theories/Init/PeanoSyntax.v @@ -21,20 +21,21 @@ Delimits Scope nat_scope with N. (* For parsing/printing based on scopes *) Module nat_scope. -Infix LEFTA 4 "+" plus : nat_scope. -Infix LEFTA 3 "*" mult : nat_scope. -Infix 5 "<=" le : nat_scope. -Infix 5 "<" lt : nat_scope. -Infix 5 ">=" ge : nat_scope. -(* Infix 5 ">" gt : nat_scope. (* Conflicts with "<..>Cases ... " *) *) +Infix "+" plus (at level 4) : nat_scope. +Infix "*" mult (at level 3): nat_scope. +Infix "<=" le (at level 5, no associativity) : nat_scope. +Infix "<" lt (at level 5, no associativity) : nat_scope. +Infix ">=" ge (at level 5, no associativity) : nat_scope. +Infix ">" gt (at level 5, no associativity) : nat_scope. (* Warning: this hides sum and prod and breaks sumor symbolic notation *) Open Scope nat_scope. +(* Syntax constr level 0: S' [ (S $p) ] -> [$p:"nat_printer_S":9] | O' [ O ] -> [ _:"nat_printer_O" ] . - +*) End nat_scope. |