diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2014-04-06 12:41:26 -0400 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2014-04-09 01:05:48 -0400 |
| commit | aa3b8b7b24e809b379fcc86f2b21ae4380b211d5 (patch) | |
| tree | 254b9d84ee42798a513bcd5aea032a6e552b2067 /kernel/retroknowledge.mli | |
| parent | de61c7d77e49286622c4aebd56f2e87b0df93903 (diff) | |
Partial support for open terms in int31.
Diffstat (limited to 'kernel/retroknowledge.mli')
| -rw-r--r-- | kernel/retroknowledge.mli | 20 |
1 files changed, 12 insertions, 8 deletions
diff --git a/kernel/retroknowledge.mli b/kernel/retroknowledge.mli index 097d207e4..ff084f71b 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 |