aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel/cbytegen.mli
diff options
context:
space:
mode:
authorGravatar Matthieu Sozeau <matthieu.sozeau@inria.fr>2015-01-15 18:45:27 +0530
committerGravatar Matthieu Sozeau <matthieu.sozeau@inria.fr>2015-01-15 18:59:00 +0530
commit8309a98096facfba448c9d8d298ba3903145831a (patch)
tree38a09851cb687921193b4368a93eed34ccd55a58 /kernel/cbytegen.mli
parent58153a5bc59bbde6534425d66a2fe5d9943eb44b (diff)
Correct restriction of vm_compute when handling universe polymorphic
definitions. Instead of failing with an anomaly when trying to do conversion or computation with the vm's, consider polymorphic constants as being opaque and keep instances around. This way the code is still correct but (obviously) incomplete for polymorphic definitions and we avoid introducing an anomaly. The patch does nothing clever, it only keeps around instances with constants/inductives and compile constant bodies only for non-polymorphic definitions.
Diffstat (limited to 'kernel/cbytegen.mli')
-rw-r--r--kernel/cbytegen.mli4
1 files changed, 2 insertions, 2 deletions
diff --git a/kernel/cbytegen.mli b/kernel/cbytegen.mli
index d0bfd46c0..eab36d8b2 100644
--- a/kernel/cbytegen.mli
+++ b/kernel/cbytegen.mli
@@ -13,7 +13,7 @@ val compile_constant_body : env -> constant_def -> body_code
(** Shortcut of the previous function used during module strengthening *)
-val compile_alias : constant -> body_code
+val compile_alias : pconstant -> body_code
(** spiwack: this function contains the information needed to perform
the static compilation of int31 (trying and obtaining
@@ -33,7 +33,7 @@ val dynamic_int31_compilation : bool -> comp_env ->
works as follow: checks if all the arguments are non-pointers
if they are applies the operation (second argument) if not
all of them are, returns to a coq definition (third argument) *)
-val op_compilation : int -> instruction -> constant -> bool -> comp_env ->
+val op_compilation : int -> instruction -> pconstant -> bool -> comp_env ->
constr array -> int -> bytecodes-> bytecodes
(*spiwack: compiling function to insert dynamic decompilation before