diff options
| author | Jason Gross | 2018-08-23 11:03:29 -0400 |
|---|---|---|
| committer | Jason Gross | 2018-08-31 20:05:54 -0400 |
| commit | 6dcbbeb95682bbf470e58e25e0a357a84c3283b6 (patch) | |
| tree | 41abb312099ed7481e16462107f3790b4295f8fb /theories/ZArith | |
| parent | 548976ac825298f27e6be00bbbb1be0752568f6f (diff) | |
Make Numeral Notation follow Import, not Require
Because that's the sane thing to do.
This will inevitably cause issues for projects which do not `Import
Coq.Strings.Ascii` before trying to use ascii notations.
We also move the syntax plugin for `int31` notations from `Cyclic31` to
`Int31`, so that users (like CompCert) who merely `Require Import
Coq.Numbers.Cyclic.Int31.Int31` get the `int31` numeral syntax. Since
`Cyclic31` `Export`s `Int31`, this should not cause any additional
incompatibilities.
Diffstat (limited to 'theories/ZArith')
| -rw-r--r-- | theories/ZArith/BinInt.v | 2 | ||||
| -rw-r--r-- | theories/ZArith/BinIntDef.v | 3 |
2 files changed, 5 insertions, 0 deletions
diff --git a/theories/ZArith/BinInt.v b/theories/ZArith/BinInt.v index cf7397b57e..a11d491a8b 100644 --- a/theories/ZArith/BinInt.v +++ b/theories/ZArith/BinInt.v @@ -1248,6 +1248,8 @@ Bind Scope Z_scope with Z.t Z. (** Re-export Notations *) +Numeral Notation Z Z.of_int Z.to_int : Z_scope. + Infix "+" := Z.add : Z_scope. Notation "- x" := (Z.opp x) : Z_scope. Infix "-" := Z.sub : Z_scope. diff --git a/theories/ZArith/BinIntDef.v b/theories/ZArith/BinIntDef.v index 8abcd15700..8cb62622db 100644 --- a/theories/ZArith/BinIntDef.v +++ b/theories/ZArith/BinIntDef.v @@ -639,6 +639,9 @@ Definition lxor a b := | neg a, neg b => of_N (N.lxor (Pos.pred_N a) (Pos.pred_N b)) end. +Numeral Notation Z of_int to_int : Z_scope. + End Z. +(** Re-export the notation for those who just [Import BinIntDef] *) Numeral Notation Z Z.of_int Z.to_int : Z_scope. |