aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel/retroknowledge.ml
diff options
context:
space:
mode:
authorGravatar Emilio Jesus Gallego Arias <e+git@x80.org>2017-11-06 23:27:09 +0100
committerGravatar Emilio Jesus Gallego Arias <e+git@x80.org>2017-11-06 23:46:52 +0100
commit03e21974a3e971a294533bffb81877dc1bd270b6 (patch)
tree1b37339378f6bc93288b61f707efb6b08f992dc5 /kernel/retroknowledge.ml
parentf3abbc55ef160d1a65d4467bfe9b25b30b965a46 (diff)
[api] Move structures deprecated in the API to the core.
We do up to `Term` which is the main bulk of the changes.
Diffstat (limited to 'kernel/retroknowledge.ml')
-rw-r--r--kernel/retroknowledge.ml6
1 files changed, 3 insertions, 3 deletions
diff --git a/kernel/retroknowledge.ml b/kernel/retroknowledge.ml
index 5fbd914f3..88cf93acc 100644
--- a/kernel/retroknowledge.ml
+++ b/kernel/retroknowledge.ml
@@ -14,7 +14,7 @@
for evaluation in the bytecode virtual machine *)
open Names
-open Term
+open Constr
(* The retroknowledge defines a bijective correspondance between some
[entry]-s (which are, in fact, merely terms) and [field]-s which
@@ -102,7 +102,7 @@ module Reactive = Map.Make (EntryOrd)
type reactive_info = {(*information required by the compiler of the VM *)
vm_compiling :
(*fastcomputation flag -> continuation -> result *)
- (bool->Cbytecodes.comp_env->constr array ->
+ (bool -> Cbytecodes.comp_env -> constr array ->
int->Cbytecodes.bytecodes->Cbytecodes.bytecodes)
option;
vm_constant_static :
@@ -117,7 +117,7 @@ type reactive_info = {(*information required by the compiler of the VM *)
(* fastcomputation flag -> cont -> result *)
vm_before_match : (bool -> Cbytecodes.bytecodes -> Cbytecodes.bytecodes) option;
(* tag (= compiled int for instance) -> result *)
- vm_decompile_const : (int -> Term.constr) option;
+ vm_decompile_const : (int -> constr) option;
native_compiling :
(bool -> Nativeinstr.prefix -> Nativeinstr.lambda array ->