From aa3b8b7b24e809b379fcc86f2b21ae4380b211d5 Mon Sep 17 00:00:00 2001
From: Maxime Dénès <mail@maximedenes.fr>
Date: Sun, 6 Apr 2014 12:41:26 -0400
Subject: Partial support for open terms in int31.

---
 kernel/uint31.mli | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

(limited to 'kernel/uint31.mli')

diff --git a/kernel/uint31.mli b/kernel/uint31.mli
index fdfb2d95a..e8b980809 100644
--- a/kernel/uint31.mli
+++ b/kernel/uint31.mli
@@ -36,4 +36,6 @@ val compare : t -> t -> int
       (* head and tail *)
 val head0   : t -> t
 val tail0   : t -> t
-  
+
+(** Used by retroknowledge *)
+val add_digit : t -> t -> t
-- 
cgit v1.2.3