aboutsummaryrefslogtreecommitdiff
path: root/theories/Numbers
diff options
context:
space:
mode:
Diffstat (limited to 'theories/Numbers')
-rw-r--r--theories/Numbers/BinNums.v1
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.