From 68304575dd3fd85d26e2f1bdff84721df8481952 Mon Sep 17 00:00:00 2001
From: Vincent Laporte
Date: Fri, 12 Oct 2018 12:22:43 +0000
Subject: [Numeral notations] Use Coqlib registered constants

---
 theories/Numbers/BinNums.v | 1 +
 1 file changed, 1 insertion(+)

(limited to 'theories/Numbers')

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.
-- 
cgit v1.2.3