diff options
| author | Emilio Jesus Gallego Arias | 2019-01-31 01:22:34 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2019-01-31 01:22:34 +0100 |
| commit | 81c6a88eb261c9e130aff73f2d5bc1ee1f7e0758 (patch) | |
| tree | 630b87fb58170e8ea756857d694eec44f6c5cddc /theories/Numbers | |
| parent | bae97b8d592dd1a5a92236959264c57ef9c57f53 (diff) | |
| parent | 0fdc5394c1f0821ae343beb8714d838c89aa4fd0 (diff) | |
Merge PR #8720: [Numeral notations] Use Coqlib registered constants
Reviewed-by: JasonGross
Ack-by: SkySkimmer
Reviewed-by: Zimmi48
Reviewed-by: ejgallego
Ack-by: ppedrot
Ack-by: vbgl
Diffstat (limited to 'theories/Numbers')
| -rw-r--r-- | theories/Numbers/BinNums.v | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/theories/Numbers/BinNums.v b/theories/Numbers/BinNums.v index ef2c688759..247827597a 100644 --- a/theories/Numbers/BinNums.v +++ b/theories/Numbers/BinNums.v @@ -29,6 +29,7 @@ Bind Scope positive_scope with positive. Arguments xO _%positive. Arguments xI _%positive. +Register positive as num.pos.type. Register xI as num.pos.xI. Register xO as num.pos.xO. Register xH as num.pos.xH. |