diff options
| author | Maxime Dénès | 2014-04-05 19:51:04 -0400 |
|---|---|---|
| committer | Maxime Dénès | 2014-04-09 01:05:48 -0400 |
| commit | de61c7d77e49286622c4aebd56f2e87b0df93903 (patch) | |
| tree | d7038f72ed54e3cdebae620c458e3ca93294f49f /kernel/nativecode.ml | |
| parent | 5bcfa8cab56798f2b575b839fd92b0f743c3d453 (diff) | |
Had to split Nativelambda in two files because of Retroknowledge
dependencies.
Diffstat (limited to 'kernel/nativecode.ml')
| -rw-r--r-- | kernel/nativecode.ml | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/kernel/nativecode.ml b/kernel/nativecode.ml index 511bb5f77e..c294345e8b 100644 --- a/kernel/nativecode.ml +++ b/kernel/nativecode.ml @@ -12,6 +12,7 @@ open Context open Declarations open Util open Nativevalues +open Nativeinstr open Nativelambda open Pre_env |