From 86357b63200368c818bbade20f2d71a3ddbaacb5 Mon Sep 17 00:00:00 2001
From: mdenes
Date: Mon, 25 Mar 2013 14:41:06 +0000
Subject: Native compiler: hash-consing of generated code and values.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16363 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 kernel/nativevalues.mli | 6 ++++++
 1 file changed, 6 insertions(+)

(limited to 'kernel/nativevalues.mli')

diff --git a/kernel/nativevalues.mli b/kernel/nativevalues.mli
index 3994f53fd1..c8adb07e50 100644
--- a/kernel/nativevalues.mli
+++ b/kernel/nativevalues.mli
@@ -29,10 +29,16 @@ type annot_sw = {
     asw_prefix : string
   }
 
+val eq_annot_sw : annot_sw -> annot_sw -> bool
+
+val hash_annot_sw : annot_sw -> int
+
 type sort_annot = string * int
       
 type rec_pos = int array
 
+val eq_rec_pos : rec_pos -> rec_pos -> bool
+
 type atom =
   | Arel of int
   | Aconstant of constant
-- 
cgit v1.2.3