diff options
| author |  Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2015-01-15 18:45:27 +0530 |
|---|---|---|
| committer | Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2015-01-15 18:59:00 +0530 |
| commit | 8309a98096facfba448c9d8d298ba3903145831a (patch) | |
| tree | 38a09851cb687921193b4368a93eed34ccd55a58 /kernel/cbytecodes.mli | |
| parent | 58153a5bc59bbde6534425d66a2fe5d9943eb44b (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/cbytecodes.mli')
| -rw-r--r-- | kernel/cbytecodes.mli | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/kernel/cbytecodes.mli b/kernel/cbytecodes.mli index 225198fcc..b65268f72 100644 --- a/kernel/cbytecodes.mli +++ b/kernel/cbytecodes.mli @@ -23,7 +23,7 @@ val cofix_evaluated_tag : tag type structured_constant = | Const_sorts of sorts - | Const_ind of inductive + | Const_ind of pinductive | Const_b0 of tag | Const_bn of tag * structured_constant array @@ -60,7 +60,7 @@ type instruction = (** nb fv, init, lbl types, lbl bodies *) | Kclosurecofix of int * int * Label.t array * Label.t array (** nb fv, init, lbl types, lbl bodies *) - | Kgetglobal of constant + | Kgetglobal of pconstant | Kconst of structured_constant | Kmakeblock of int * tag (** size, tag *) | Kmakeprod |