diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-04-09 11:27:06 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-04-09 11:27:06 +0000 |
| commit | af0f51807d1e4765c97d4a39494b04268121bae3 (patch) | |
| tree | 0c6f6fb65866ced4e631b31142821e970f95b546 /theories/ZArith | |
| parent | a0f0f3982bf6991407f399ac430b354375a48dd2 (diff) | |
Suppression de l'étage "Import nat/Z/R_scope". "Open Scope" remplace "Import"
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3881 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/ZArith')
| -rw-r--r-- | theories/ZArith/Zsyntax.v | 25 |
1 files changed, 14 insertions, 11 deletions
diff --git a/theories/ZArith/Zsyntax.v b/theories/ZArith/Zsyntax.v index 81c0d9817..757b539ab 100644 --- a/theories/ZArith/Zsyntax.v +++ b/theories/ZArith/Zsyntax.v @@ -221,18 +221,9 @@ Syntax constr ]. (* For parsing/printing based on scopes *) +V7only [ Module Z_scope. - -(* Declare Scope positive_scope with Key P. *) - -Delimits Scope positive_scope with P. -Delimits Scope Z_scope with Z. - -(* Warning: this hides sum and prod and breaks sumor symbolic notation *) -Open Scope Z_scope. - -Arguments Scope POS [positive_scope]. -Arguments Scope NEG [positive_scope]. +]. Infix LEFTA 4 "+" Zplus : Z_scope. Infix LEFTA 4 "-" Zminus : Z_scope. @@ -272,4 +263,16 @@ Syntax constr level 0: Zeq [ (eq Z $n1 $n2) ] -> [[<hov 0> $n1 [1 0] "= " $n2 ]]. ]. +V7only [ +Open Scope Z_scope. End Z_scope. +]. + +(* Declare Scope positive_scope with Key P. *) + +Delimits Scope positive_scope with P. +Delimits Scope Z_scope with Z. + +Arguments Scope POS [positive_scope]. +Arguments Scope NEG [positive_scope]. + |