diff options
| -rw-r--r-- | contrib/correctness/Sorted.v | 2 | ||||
| -rwxr-xr-x | contrib/omega/Omega.v | 4 | ||||
| -rwxr-xr-x | theories/Init/Peano.v | 25 | ||||
| -rw-r--r-- | theories/Init/PeanoSyntax.v | 24 | ||||
| -rw-r--r-- | theories/Reals/Rsyntax.v | 13 | ||||
| -rw-r--r-- | theories/ZArith/Zsyntax.v | 25 |
6 files changed, 51 insertions, 42 deletions
diff --git a/contrib/correctness/Sorted.v b/contrib/correctness/Sorted.v index 73179ed1e..8c3743a1e 100644 --- a/contrib/correctness/Sorted.v +++ b/contrib/correctness/Sorted.v @@ -15,7 +15,7 @@ Require ArrayPermut. Require ZArithRing. Require Omega. -Import Z_scope. +V7only [Import Z_scope.]. Set Implicit Arguments. diff --git a/contrib/omega/Omega.v b/contrib/omega/Omega.v index 84ede032b..70ede13d0 100755 --- a/contrib/omega/Omega.v +++ b/contrib/omega/Omega.v @@ -30,8 +30,10 @@ Hints Resolve Zle_n Zplus_sym Zplus_assoc Zmult_sym Zmult_assoc Require Export Zhints. +(* (* The constant minus is required in coq_omega.ml *) -Require Export Minus. +Require Minus. +*) Hint eq_nat_Omega : zarith := Extern 10 (eq nat ? ?) Abstract Omega. Hint le_Omega : zarith := Extern 10 (le ? ?) Abstract Omega. diff --git a/theories/Init/Peano.v b/theories/Init/Peano.v index a3774efb6..0cb7edd7f 100755 --- a/theories/Init/Peano.v +++ b/theories/Init/Peano.v @@ -174,3 +174,28 @@ Proof. Induction n; Auto. Induction m; Auto. Qed. + +(** Notations *) +V7only[ +Syntax constr + level 0: + S [ (S $p) ] -> [$p:"nat_printer":9] + | O [ O ] -> ["(0)"]. +]. +V7only [ +Module nat_scope. +]. + +(* For parsing/printing based on scopes *) +Infix 4 "+" plus : nat_scope V8only (left associativity). +Infix 4 "-" minus : nat_scope V8only (left associativity). +Infix 3 "*" mult : nat_scope V8only (left associativity). +Infix NONA 5 "<=" le : nat_scope. +Infix NONA 5 "<" lt : nat_scope. +Infix NONA 5 ">=" ge : nat_scope. +Infix NONA 5 ">" gt : nat_scope. + +V7only [ +End nat_scope. +]. +Delimits Scope nat_scope with N. diff --git a/theories/Init/PeanoSyntax.v b/theories/Init/PeanoSyntax.v index 072be35dd..3b7b91454 100644 --- a/theories/Init/PeanoSyntax.v +++ b/theories/Init/PeanoSyntax.v @@ -10,27 +10,3 @@ Require Datatypes. Require Peano. -V7only[ -Syntax constr - level 0: - S [ (S $p) ] -> [$p:"nat_printer":9] - | O [ O ] -> ["(0)"]. -]. -(* Outside the module to be able to parse the grammar for 0,1,2... !! *) -Delimits Scope nat_scope with N. - -(* For parsing/printing based on scopes *) -Module nat_scope. - -(* Warning: this hides sum and prod and breaks sumor symbolic notation *) -Open Scope nat_scope. - -Infix 4 "+" plus : nat_scope V8only (left associativity). -Infix 4 "-" minus : nat_scope V8only (left associativity). -Infix 3 "*" mult : nat_scope V8only (left associativity). -Infix NONA 5 "<=" le : nat_scope. -Infix NONA 5 "<" lt : nat_scope. -Infix NONA 5 ">=" ge : nat_scope. -Infix NONA 5 ">" gt : nat_scope. - -End nat_scope. diff --git a/theories/Reals/Rsyntax.v b/theories/Reals/Rsyntax.v index 8b209bde2..b08ef8272 100644 --- a/theories/Reals/Rsyntax.v +++ b/theories/Reals/Rsyntax.v @@ -197,12 +197,9 @@ Syntax constr . ]. (* For parsing/printing based on scopes *) +V7only [ Module R_scope. - -Delimits Scope R_scope with R. - -(* Warning: this hides sum and prod and breaks sumor symbolic notation *) -Open Scope R_scope. +]. Infix "<=" Rle (at level 5, no associativity) : R_scope. Infix "<" Rlt (at level 5, no associativity) : R_scope. @@ -237,4 +234,10 @@ Notation "x <> y" := ~(eqT R x y) (at level 5) : R_scope. Notation "/ x" := (Rinv x) (at level 0): R_scope V8only (at level 30, left associativity). +V7only [ +Open Scope R_scope. End R_scope. +]. + +Delimits Scope R_scope with R. + 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]. + |