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/NArith | |
| 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/NArith')
| -rw-r--r-- | theories/NArith/BinNat.v | 2 | ||||
| -rw-r--r-- | theories/NArith/BinNatDef.v | 3 |
2 files changed, 5 insertions, 0 deletions
diff --git a/theories/NArith/BinNat.v b/theories/NArith/BinNat.v index 5d3ec5abc7..bd27f94abd 100644 --- a/theories/NArith/BinNat.v +++ b/theories/NArith/BinNat.v @@ -930,6 +930,8 @@ Bind Scope N_scope with N.t N. (** Exportation of notations *) +Numeral Notation N N.of_uint N.to_uint : N_scope. + Infix "+" := N.add : N_scope. Infix "-" := N.sub : N_scope. Infix "*" := N.mul : N_scope. diff --git a/theories/NArith/BinNatDef.v b/theories/NArith/BinNatDef.v index 8bbecf9acb..be12fffaaf 100644 --- a/theories/NArith/BinNatDef.v +++ b/theories/NArith/BinNatDef.v @@ -402,6 +402,9 @@ Definition to_uint n := Definition to_int n := Decimal.Pos (to_uint n). +Numeral Notation N of_uint to_uint : N_scope. + End N. +(** Re-export the notation for those who just [Import NatIntDef] *) Numeral Notation N N.of_uint N.to_uint : N_scope. |