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

---
 kernel/retroknowledge.mli | 20 ++++++++++++--------
 1 file changed, 12 insertions(+), 8 deletions(-)

(limited to 'kernel/retroknowledge.mli')

diff --git a/kernel/retroknowledge.mli b/kernel/retroknowledge.mli
index 097d207e4f..ff084f71bf 100644
--- a/kernel/retroknowledge.mli
+++ b/kernel/retroknowledge.mli
@@ -6,6 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+open Names
 open Term
 
 type retroknowledge
@@ -122,12 +123,12 @@ val get_native_compiling_info  : retroknowledge -> entry -> Cbytecodes.comp_env
                              int -> Cbytecodes.bytecodes-> Cbytecodes.bytecodes
 
 val get_native_constant_static_info : retroknowledge -> entry ->
-                                   constr array -> Nativeinstr.lambda
+                                      constr array -> Nativeinstr.lambda
 
 val get_native_constant_dynamic_info : retroknowledge -> entry ->
-                                Cbytecodes.comp_env ->
-                                Cbytecodes.block array ->
-                                int -> Cbytecodes.bytecodes -> Cbytecodes.bytecodes
+                                       Nativeinstr.prefix -> constructor ->
+				       Nativeinstr.lambda array ->
+				       Nativeinstr.lambda
 
 val get_native_before_match_info : retroknowledge -> entry -> Cbytecodes.bytecodes
                                                        -> Cbytecodes.bytecodes
@@ -168,15 +169,18 @@ val add_native_compiling_info : retroknowledge-> entry ->
                             (bool -> Cbytecodes.comp_env -> constr array -> int ->
                             Cbytecodes.bytecodes -> Cbytecodes.bytecodes) ->
                             retroknowledge
+
 val add_native_constant_static_info : retroknowledge -> entry ->
                                   (bool -> constr array ->
                                       Nativeinstr.lambda) ->
                                   retroknowledge
-val add_native_constant_dynamic_info : retroknowledge-> entry ->
-                                   (bool -> Cbytecodes.comp_env ->
-                                   Cbytecodes.block array -> int ->
-                                   Cbytecodes.bytecodes -> Cbytecodes.bytecodes) ->
+
+val add_native_constant_dynamic_info : retroknowledge -> entry ->
+                                   (bool -> Nativeinstr.prefix -> constructor ->
+				      Nativeinstr.lambda array ->
+				      Nativeinstr.lambda) ->
                                    retroknowledge
+
 val add_native_before_match_info : retroknowledge -> entry ->
                               (bool->Cbytecodes.bytecodes->Cbytecodes.bytecodes) ->
                               retroknowledge
-- 
cgit v1.2.3